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

Back to dedukti v2.2c

parent 50dd5f09
......@@ -6,8 +6,8 @@ bool : cc.uT.
Bool : Type := cc.eT bool.
(; Constructors ;)
{true} : Bool.
{false} : Bool.
true : Bool.
false : Bool.
(; Pattern-matching ;)
match :
......
#NAME dk_list.
(; Polymorphic lists ;)
{list} : cc.uT -> cc.uT.
list : cc.uT -> cc.uT.
List := A : cc.uT => cc.eT (list A).
(; Constructors ;)
{nil} : A : cc.uT -> List A.
{cons} : A : cc.uT -> cc.eT A -> List A -> List A.
nil : A : cc.uT -> List A.
cons : A : cc.uT -> cc.eT A -> List A -> List A.
(; Case distinction ;)
match : A : cc.uT ->
......
......@@ -4,8 +4,8 @@ Bool : Type := dk_bool.Bool.
nat : cc.uT.
Nat : Type := cc.eT nat.
{O} : Nat.
{S} : Nat -> Nat.
O : Nat.
S : Nat -> Nat.
(; Order ;)
lt : Nat -> Nat -> Bool.
......
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