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

Try using rewrite rule on cc.eT in a file different from cc (does not

yet work)
parent ce755964
......@@ -15,9 +15,6 @@ def Arrow : uT -> uT -> uT.
(; See dk_type ;)
(; Cartesian product ;)
Prod : uT -> uT -> Type.
prod : uT -> uT -> uT.
[X,Y] eT (prod X Y) --> Prod X Y.
(; Dependant sum ;)
Sigma : A : uT -> (eT A -> uT) -> Type.
......
......@@ -23,7 +23,7 @@ def eeP : Prop -> cc.uT.
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) --> cc.prod (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)
[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)).
......
#NAME dk_tuple.
(; Kept for backward compatibility, see dk_type ;)
def tuple := cc.prod.
def tuple := dk_type.prod.
def Tuple := dk_type.Prod.
def cpl := dk_type.cpl.
def fst := dk_type.fst.
......
......@@ -3,7 +3,9 @@
(; Basics type constructs. ;)
(; Cartesian product ;)
def Prod := cc.Prod.
Prod : cc.uT -> cc.uT -> Type.
prod : cc.uT -> cc.uT -> cc.uT.
[X,Y] cc.eT (prod X Y) --> Prod X Y.
cpl : A : cc.uT ->
B : cc.uT ->
......
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