Commit edca5a50 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Renumbering examples

parent 59d3e2f0
......@@ -6,6 +6,12 @@ type_cons := dk_obj.Ot_cons.
type_nil := dk_obj.Ot_nil.
Expr := dk_obj.Expr.
nat : type.
Nat := Expr nat.
42 : Nat.
24 : Nat.
(; Booleans ;)
l_if : Label
......@@ -175,7 +181,7 @@ App : A : type ->
(self : Arrow A B => a))
l_val.
test7 :=
test3 :=
A : type =>
a : Expr A =>
b : Expr A =>
......@@ -185,33 +191,6 @@ test7 :=
(Lambda A A (x : Expr A => b))
a.
(; Subtyping example ;)
l_get := dk_string.cons dk_char.g (
dk_string.cons dk_char.e (
dk_string.cons dk_char.t (
dk_string.nil))).
l_set := dk_string.cons dk_char.s (
dk_string.cons dk_char.e (
dk_string.cons dk_char.t (
dk_string.nil))).
l_contents := dk_string.cons dk_char.c (
dk_string.cons dk_char.o (
dk_string.cons dk_char.n (
dk_string.cons dk_char.t (
dk_string.cons dk_char.e (
dk_string.cons dk_char.n (
dk_string.cons dk_char.t (
dk_string.cons dk_char.s (
dk_string.nil)))))))).
nat : type.
Nat := Expr nat.
42 : Nat.
24 : Nat.
(; Points and color points ;)
l_x := dk_string.cons dk_char.x dk_string.nil.
......@@ -250,7 +229,29 @@ myPoint : Point
l_c
(s : ColorPoint => red)).
test9 : Nat := dk_obj.select point myPoint l_x.
test4 : Nat := dk_obj.select point myPoint l_x.
(; Subtyping example ;)
l_get := dk_string.cons dk_char.g (
dk_string.cons dk_char.e (
dk_string.cons dk_char.t (
dk_string.nil))).
l_set := dk_string.cons dk_char.s (
dk_string.cons dk_char.e (
dk_string.cons dk_char.t (
dk_string.nil))).
l_contents := dk_string.cons dk_char.c (
dk_string.cons dk_char.o (
dk_string.cons dk_char.n (
dk_string.cons dk_char.t (
dk_string.cons dk_char.e (
dk_string.cons dk_char.n (
dk_string.cons dk_char.t (
dk_string.cons dk_char.s (
dk_string.nil)))))))).
(; Storage cells ;)
......@@ -294,7 +295,7 @@ myRom : RomCell
l_get
(self : RomCell => 42)).
test3 := dk_obj.select romCell myRom l_get.
test5 := dk_obj.select romCell myRom l_get.
myProm : PromCell
:=
......@@ -316,8 +317,8 @@ myProm : PromCell
l_get
(s : PromCell => x)))).
test4 := dk_obj.select promCell myProm l_get.
test5 := dk_obj.select
test6 := dk_obj.select promCell myProm l_get.
test7 := dk_obj.select
romCell
(App nat romCell (dk_obj.select promCell myProm l_set) 24)
l_get.
......@@ -351,7 +352,7 @@ myCell : PromCell
l_contents
(self : PrivateCell => 42)).
test6 := dk_obj.select
test8 := dk_obj.select
romCell
(App nat romCell
(dk_obj.select
......@@ -361,11 +362,4 @@ test6 := dk_obj.select
24)
l_get.
test8 := dk_obj.select promCell myCell l_contents.
(; #SNF test1. ;)
(; #SNF test2. ;)
(; #SNF test3. ;)
(; #SNF test4. ;)
(; #SNF test5. ;)
(; #SNF test6. ;)
test9 := dk_obj.select promCell myCell l_contents.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment