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

Rewrite rules on external symbols now work! (Thank you Ronan!).

Move rules on cc.eT to better locations so that cc.dk only talk about
dependent product and arrow.
parent b3340880
......@@ -9,40 +9,3 @@ Pi : X : uT -> ((eT X) -> uT) -> uT.
def Arrow : uT -> uT -> uT.
[t1,t2] Arrow t1 t2 --> Pi t1 (x : eT t1 => t2).
(; Declaration of some types which need to add rules on eT. ;)
(; See dk_type ;)
(; Cartesian product ;)
(; Dependant sum ;)
Sigma : A : uT -> (eT A -> uT) -> Type.
sigma : A : uT -> (eT A -> uT) -> uT.
[X,Y] eT (sigma X Y) --> Sigma X Y.
(; Binary sum ;)
Sum : uT -> uT -> Type.
sum : uT -> uT -> uT.
[X,Y] eT (sum X Y) --> Sum X Y.
(; See dk_list ;)
(; Lists ;)
List : uT -> Type.
list : uT -> uT.
[A] eT (list A) --> List A.
(; See dk_nat ;)
Nat : Type.
nat : uT.
[] eT nat --> Nat.
(; See dk_machine_int ;)
MInt : Nat -> Type.
Mint : Nat -> uT.
[N] eT (Mint N) --> MInt N.
(; See dk_opt ;)
Option : uT -> Type.
option : uT -> uT.
[A] eT (option A) --> Option A.
#NAME dk_list.
(; Polymorphic lists ;)
def list : cc.uT -> cc.uT := cc.list.
def List : cc.uT -> Type := cc.List.
list : cc.uT -> cc.uT.
List : cc.uT -> Type.
[A] cc.eT (list A) --> List A.
(; Constructors ;)
nil : A : cc.uT -> List A.
......
......@@ -24,9 +24,9 @@ def eP : Prop -> Type
:= f : Prop => cc.eT (eeP f).
[f1,f2] eeP (imp f1 f2) --> cc.Arrow (eeP f1) (eeP f2)
[f1,f2] eeP (and f1 f2) --> dk_type.prod (eeP f1) (eeP f2)
[f1,f2] eeP (or f1 f2) --> cc.sum (eeP f1) (eeP f2)
[f1,f2] eeP (or f1 f2) --> dk_type.sum (eeP f1) (eeP f2)
[A,f] eeP (forall A f) --> cc.Pi A (x : cc.eT A => eeP (f x))
[A,f] eeP (exists A f) --> cc.sigma A (x : cc.eT A => eeP (f x)).
[A,f] eeP (exists A f) --> dk_type.sigma A (x : cc.eT A => eeP (f x)).
......
......@@ -5,8 +5,9 @@ def UNat : Type := dk_nat.Nat.
def UO : UNat := dk_nat.O.
def US : UNat -> UNat := dk_nat.S.
def Mint := cc.Mint.
def MInt := cc.MInt.
Mint : UNat -> cc.uT.
MInt : UNat -> Type.
[N] cc.eT (Mint N) --> MInt N.
O : MInt UO.
S0 : N : UNat -> MInt N -> MInt (US N).
......
......@@ -74,7 +74,10 @@ Some : A : cc.uT -> cc.eT A -> cc.eT (option A).
(; list type ;)
def list := cc.list.
list : cc.uT -> cc.uT.
List : cc.uT -> Type.
[A] cc.eT (list A) --> List A.
Nil : A : cc.uT -> cc.eT (list A).
Cons : A : cc.uT -> cc.eT A -> cc.eT (list A) -> cc.eT (list A).
......
#NAME dk_nat.
def Bool : Type := dk_bool.Bool.
def nat := cc.nat.
def Nat := cc.Nat.
nat : cc.uT.
Nat : Type.
[] cc.eT nat --> Nat.
O : Nat.
S : Nat -> Nat.
......
#NAME dk_opt.
(; options ;)
def option := cc.option.
def Option := cc.Option.
option : cc.uT -> cc.uT.
Option : cc.uT -> Type.
[A] cc.eT (option A) --> Option A.
None : A : cc.uT -> Option A.
Some : A : cc.uT -> cc.eT A -> Option A.
......
......@@ -21,8 +21,9 @@ def snd : A : cc.uT -> B : cc.uT -> Prod A B -> cc.eT B.
(; Dependent product ;)
def sigma := cc.sigma.
def Sigma := cc.Sigma.
Sigma : A : cc.uT -> (cc.eT A -> cc.uT) -> Type.
sigma : A : cc.uT -> (cc.eT A -> cc.uT) -> cc.uT.
[X,Y] cc.eT (sigma X Y) --> Sigma X Y.
dcpl : A : cc.uT ->
B : (cc.eT A -> cc.uT) ->
......@@ -45,8 +46,9 @@ def dsnd : A : cc.uT ->
(; Sum ;)
def sum := cc.sum.
def Sum := cc.Sum.
Sum : cc.uT -> cc.uT -> Type.
sum : cc.uT -> cc.uT -> cc.uT.
[X,Y] cc.eT (sum X Y) --> Sum X Y.
left (A : cc.uT) (B : cc.uT) : cc.eT A -> Sum A B.
right (A : cc.uT) (B : cc.uT) : cc.eT B -> Sum A B.
......
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