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

Use Sukerujo syntax for easier debugging

parent 5d4ca41a
.bkp/
*.dko
*.dk
!builtins.dk
.depend
tmp.dk
_build/
*.native
*.byte
*.glob
*.vo
test.dk
test.sk
test.v
sigmaid
README.html
......@@ -30,8 +30,9 @@
# The fact that you are presently reading this means that you have had
# knowledge of the CeCILL-B license and that you accept its terms.
DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko)
SKS = $(wildcard *.sk)
DKS = $(SKS:.sk=.dk)
DKOS = $(SKS:.sk=.dko)
# Change COMPILE_MODE to byte if you want bytecode
# instead of machine code
......@@ -41,16 +42,26 @@ COMPILE_MODE = native
INSTALL_DIR = /usr/local/bin
.PHONY: clean depend
.SUFFIXES: .dk .dko .ml .native .byte .v .vo
.SUFFIXES: .dk .sk .dko .ml .native .byte .v .vo
DKCHECK=dkcheck
SKINDENT=skindent
DKDEP=dkdep
DKCHECKOPTIONS=-nl
CONFLUENCECHECKER=$(shell locate csiho.sh)
DKCHECKOPTIONS=-nl -errors-in-snf -v -d # -cc $(CONFLUENCECHECKER)
DKDEPOPTIONS=-v
.dk.dko:
all: $(DKOS) sigmaid
builtins.dko: builtins.dk
$(DKCHECK) -e $<
%.dko:
$(DKCHECK) -e $(DKCHECKOPTIONS) $<
%.dk: %.sk
$(SKINDENT) $< > $@
.v.vo:
coqc $<
......@@ -59,15 +70,13 @@ DKDEPOPTIONS=-v
.ml.byte:
ocamlbuild -use-menhir $@
all: $(DKOS) sigmaid
depend: .depend
.depend:
$(DKDEP) $(DKDEPOPTIONS) pts.dk dk_*.dk > .depend
.depend: $(DKS)
$(DKDEP) $(DKDEPOPTIONS) $(DKS) > .depend
clean:
rm -rf *.dko *.vo *.glob .depend tmp.dk \
test.dk test.v \
rm -rf *.dko pts.dk dk_*.dk *.vo *.glob .depend tmp.* \
test.sk test.v \
sigmaid sigmaid.native sigmaid.byte _build
sigmaid: sigmaid.$(COMPILE_MODE)
......@@ -76,7 +85,7 @@ sigmaid: sigmaid.$(COMPILE_MODE)
install: sigmaid
install sigmaid $(INSTALL_DIR)/
test.dk: sigmaid.$(COMPILE_MODE)
test.sk: sigmaid.$(COMPILE_MODE)
./sigmaid.$(COMPILE_MODE) test.sigma
test.v: sigmaid.$(COMPILE_MODE)
......
#NAME builtins.
nat : Type.
0 : nat.
S : nat -> nat.
char : Type.
char_of_nat : nat -> char.
string : Type.
string_nil : string.
string_cons : char -> string -> string.
......@@ -36,39 +36,36 @@ knowledge of the CeCILL-B license and that you accept its terms.
;)
def uT := pts.uT.
def eT := pts.eT.
(; Bool ;)
(; Declaration ;)
Bool : Type.
bool : Type.
(; Constructors ;)
true : Bool.
false : Bool.
true : bool.
false : bool.
(; Pattern-matching ;)
def match :
P : (Bool -> uT) ->
eT (P true) ->
eT (P false) ->
b : Bool ->
eT (P b).
P : (bool -> pts.uT) ->
pts.eT (P true) ->
pts.eT (P false) ->
b : bool ->
pts.eT (P b).
[H] match _ H _ true --> H
[H] match _ _ H false --> H.
(; boolean if .. then .. else .. ;)
def iteb : Bool -> Bool -> Bool -> Bool.
def iteb : bool -> bool -> bool -> bool.
[b] iteb true b _ --> b
[b] iteb false _ b --> b.
(; negation ;)
def not : Bool -> Bool.
def not : bool -> bool.
[b] not b --> iteb b false true.
(; binary operators ;)
def and : Bool -> Bool -> Bool.
def and : bool -> bool -> bool.
[x,y] and x y --> iteb x y false.
def or : Bool -> Bool -> Bool.
def or : bool -> bool -> bool.
[x,y] or x y --> iteb x true y.
#NAME dk_char.
(;
Copyright Raphaël Cauderlier (2014)
<raphael.cauderlier@inria.fr>
This software is a computer program whose purpose is to translate object-oriented program written in the simply-typed ς-calculus from Abadi and Cardelli to Dedukti and Coq.
This software is governed by the CeCILL-B license under French law and
abiding by the rules of distribution of free software. You can use,
modify and/ or redistribute the software under the terms of the CeCILL-B
license as circulated by CEA, CNRS and INRIA at the following URL
"http://www.cecill.info".
As a counterpart to the access to the source code and rights to copy,
modify and redistribute granted by the license, users are provided
only with a limited warranty and the software's author, the holder of
the economic rights, and the successive licensors have only limited
liability.
In this respect, the user's attention is drawn to the risks associated
with loading, using, modifying and/or developing or reproducing the
software by the user in light of its specific status of free software,
that may mean that it is complicated to manipulate, and that also
therefore means that it is reserved for developers and experienced
professionals having in-depth computer knowledge. Users are therefore
encouraged to load and test the software's suitability as regards
their requirements in conditions enabling the security of their
systems and/or data to be ensured and, more generally, to use and
operate it in the same conditions as regards security.
The fact that you are presently reading this means that you have had
knowledge of the CeCILL-B license and that you accept its terms.
;)
(; 7bits (ascii) characters ;)
def uT := pts.uT.
def eT := pts.eT.
def Char : Type := dk_machine_int.MInt dk_nat.7.
def _O : dk_binary_nat.BNat := dk_binary_nat.O.
def S0 : dk_binary_nat.BNat -> dk_binary_nat.BNat := dk_binary_nat.S0.
def S1 : dk_binary_nat.BNat -> dk_binary_nat.BNat := dk_binary_nat.S1.
def cast : dk_binary_nat.BNat -> Char := dk_machine_int.cast_bnat dk_nat.7.
def 0 : Char := cast (S0 (S0 (S0 (S0 (S1 (S1 _O)))))).
def 1 : Char := cast (S1 (S0 (S0 (S0 (S1 (S1 _O)))))).
def 2 : Char := cast (S0 (S1 (S0 (S0 (S1 (S1 _O)))))).
def 3 : Char := cast (S1 (S1 (S0 (S0 (S1 (S1 _O)))))).
def 4 : Char := cast (S0 (S0 (S1 (S0 (S1 (S1 _O)))))).
def 5 : Char := cast (S1 (S0 (S1 (S0 (S1 (S1 _O)))))).
def 6 : Char := cast (S0 (S1 (S1 (S0 (S1 (S1 _O)))))).
def 7 : Char := cast (S1 (S1 (S1 (S0 (S1 (S1 _O)))))).
def 8 : Char := cast (S0 (S0 (S0 (S1 (S1 (S1 _O)))))).
def 9 : Char := cast (S1 (S0 (S0 (S1 (S1 (S1 _O)))))).
def A : Char := cast (S1 (S0 (S0 (S0 (S0 (S0 (S1 _O))))))).
def B : Char := cast (S0 (S1 (S0 (S0 (S0 (S0 (S1 _O))))))).
def C : Char := cast (S1 (S1 (S0 (S0 (S0 (S0 (S1 _O))))))).
def D : Char := cast (S0 (S0 (S1 (S0 (S0 (S0 (S1 _O))))))).
def E : Char := cast (S1 (S0 (S1 (S0 (S0 (S0 (S1 _O))))))).
def F : Char := cast (S0 (S1 (S1 (S0 (S0 (S0 (S1 _O))))))).
def G : Char := cast (S1 (S1 (S1 (S0 (S0 (S0 (S1 _O))))))).
def H : Char := cast (S0 (S0 (S0 (S1 (S0 (S0 (S1 _O))))))).
def I : Char := cast (S1 (S0 (S0 (S1 (S0 (S0 (S1 _O))))))).
def J : Char := cast (S0 (S1 (S0 (S1 (S0 (S0 (S1 _O))))))).
def K : Char := cast (S1 (S1 (S0 (S1 (S0 (S0 (S1 _O))))))).
def L : Char := cast (S0 (S0 (S1 (S1 (S0 (S0 (S1 _O))))))).
def M : Char := cast (S1 (S0 (S1 (S1 (S0 (S0 (S1 _O))))))).
def N : Char := cast (S0 (S1 (S1 (S1 (S0 (S0 (S1 _O))))))).
def O : Char := cast (S1 (S1 (S1 (S1 (S0 (S0 (S1 _O))))))).
def P : Char := cast (S0 (S0 (S0 (S0 (S1 (S0 (S1 _O))))))).
def Q : Char := cast (S1 (S0 (S0 (S0 (S1 (S0 (S1 _O))))))).
def R : Char := cast (S0 (S1 (S0 (S0 (S1 (S0 (S1 _O))))))).
def S : Char := cast (S1 (S1 (S0 (S0 (S1 (S0 (S1 _O))))))).
def T : Char := cast (S0 (S0 (S1 (S0 (S1 (S0 (S1 _O))))))).
def U : Char := cast (S1 (S0 (S1 (S0 (S1 (S0 (S1 _O))))))).
def V : Char := cast (S0 (S1 (S1 (S0 (S1 (S0 (S1 _O))))))).
def W : Char := cast (S1 (S1 (S1 (S0 (S1 (S0 (S1 _O))))))).
def X : Char := cast (S0 (S0 (S0 (S1 (S1 (S0 (S1 _O))))))).
def Y : Char := cast (S1 (S0 (S0 (S1 (S1 (S0 (S1 _O))))))).
def Z : Char := cast (S0 (S1 (S0 (S1 (S1 (S0 (S1 _O))))))).
def a : Char := cast (S1 (S0 (S0 (S0 (S0 (S1 (S1 _O))))))).
def b : Char := cast (S0 (S1 (S0 (S0 (S0 (S1 (S1 _O))))))).
def c : Char := cast (S1 (S1 (S0 (S0 (S0 (S1 (S1 _O))))))).
def d : Char := cast (S0 (S0 (S1 (S0 (S0 (S1 (S1 _O))))))).
def e : Char := cast (S1 (S0 (S1 (S0 (S0 (S1 (S1 _O))))))).
def f : Char := cast (S0 (S1 (S1 (S0 (S0 (S1 (S1 _O))))))).
def g : Char := cast (S1 (S1 (S1 (S0 (S0 (S1 (S1 _O))))))).
def h : Char := cast (S0 (S0 (S0 (S1 (S0 (S1 (S1 _O))))))).
def i : Char := cast (S1 (S0 (S0 (S1 (S0 (S1 (S1 _O))))))).
def j : Char := cast (S0 (S1 (S0 (S1 (S0 (S1 (S1 _O))))))).
def k : Char := cast (S1 (S1 (S0 (S1 (S0 (S1 (S1 _O))))))).
def l : Char := cast (S0 (S0 (S1 (S1 (S0 (S1 (S1 _O))))))).
def m : Char := cast (S1 (S0 (S1 (S1 (S0 (S1 (S1 _O))))))).
def n : Char := cast (S0 (S1 (S1 (S1 (S0 (S1 (S1 _O))))))).
def o : Char := cast (S1 (S1 (S1 (S1 (S0 (S1 (S1 _O))))))).
def p : Char := cast (S0 (S0 (S0 (S0 (S1 (S1 (S1 _O))))))).
def q : Char := cast (S1 (S0 (S0 (S0 (S1 (S1 (S1 _O))))))).
def r : Char := cast (S0 (S1 (S0 (S0 (S1 (S1 (S1 _O))))))).
def s : Char := cast (S1 (S1 (S0 (S0 (S1 (S1 (S1 _O))))))).
def t : Char := cast (S0 (S0 (S1 (S0 (S1 (S1 (S1 _O))))))).
def u : Char := cast (S1 (S0 (S1 (S0 (S1 (S1 (S1 _O))))))).
def v : Char := cast (S0 (S1 (S1 (S0 (S1 (S1 (S1 _O))))))).
def w : Char := cast (S1 (S1 (S1 (S0 (S1 (S1 (S1 _O))))))).
def x : Char := cast (S0 (S0 (S0 (S1 (S1 (S1 (S1 _O))))))).
def y : Char := cast (S1 (S0 (S0 (S1 (S1 (S1 (S1 _O))))))).
def z : Char := cast (S0 (S1 (S0 (S1 (S1 (S1 (S1 _O))))))).
def __ : Char := cast (S1 (S0 (S1 (S1 (S1 (S1 (S1 _O))))))).
def equal : Char -> Char -> dk_bool.Bool
:= dk_machine_int.equal dk_nat.7.
def equal_refl : c : Char -> dk_logic.Istrue (equal c c)
:= dk_machine_int.equal_refl dk_nat.7.
#NAME dk_nat.
#NAME dk_char.
(;
Copyright Raphaël Cauderlier (2014)
......@@ -36,30 +35,21 @@ knowledge of the CeCILL-B license and that you accept its terms.
;)
def Bool : Type := dk_bool.Bool.
Nat : Type.
O : Nat.
S : Nat -> Nat.
(; Operations ;)
(; 7bits (ascii) characters ;)
(; Addition ;)
(; This definition of plus is compatible with dependant list concatenation ;)
def plus : Nat -> Nat -> Nat.
[m] plus O m --> m
[n,m] plus (S n) m --> S (plus n m).
def equal : char -> char -> dk_bool.bool.
[m,n] equal (char_of_nat m) (char_of_nat n) --> dk_nat.equal m n.
(; Product ;)
def mult : Nat -> Nat -> Nat.
[m] mult O m --> O
[n,m] mult (S n) m --> plus (mult n m) m.
def equal_refl : c : char -> dk_logic.Istrue (equal c c).
[n] equal_refl (char_of_nat n) --> dk_nat.equal_refl n.
def 1 := S O.
def 2 := S 1.
def 3 := S 2.
def 4 := S 3.
def 5 := S 4.
def 6 := S 5.
def 7 := S 6.
def eq_rect : c1 : char ->
c2 : char ->
P : (char -> pts.uT) ->
dk_logic.Istrue (equal c1 c2) ->
pts.eT (P c1) ->
pts.eT (P c2).
[n,m,P,H,x]
eq_rect (char_of_nat n) (char_of_nat m) P H x
-->
dk_nat.eq_rect n m (k : nat => P (char_of_nat k)) H x.
......@@ -40,11 +40,11 @@ def uT := pts.uT.
def eT := pts.eT.
def Arrow := pts.Arrow.
def Bool := dk_bool.Bool.
def true : Bool := dk_bool.true.
def false : Bool := dk_bool.false.
def not : Bool -> Bool := dk_bool.not.
def or : Bool -> Bool -> Bool
def bool := dk_bool.bool.
def true : bool := dk_bool.true.
def false : bool := dk_bool.false.
def not : bool -> bool := dk_bool.not.
def or : bool -> bool -> bool
:= dk_bool.or.
def Prop := dk_logic.Prop.
......@@ -55,30 +55,24 @@ def tt : Istrue true := dk_logic.I.
def bool_or_intro2 := dk_logic.bool_or_intro2.
(; Labels ;)
def Label := dk_string.String.
def label_eq : Label -> Label -> Bool := dk_string.equal.
(; Correctness of label_eq ;)
def label_eq_rect := dk_string.eq_rect.
(; Dependant if with equality ;)
def if_label_eq := dk_string.if_eq.
def Label := string.
def label_eq : Label -> Label -> bool := dk_string.equal.
Domain : Type.
nil : Domain.
cons : Label -> Domain -> Domain.
dnil : Domain.
dcons : Label -> Domain -> Domain.
(; Membership as predicate. ;)
position : Label -> Domain -> uT.
Position : Label -> Domain -> Type.
[l,D] pts.eT (position l D) --> Position l D.
Position_head : l : Label -> d : Domain -> Position l (cons l d).
Position_head : l : Label -> d : Domain -> Position l (dcons l d).
Position_tail : l : Label ->
l2 : Label ->
d : Domain ->
Position l d ->
Position l (cons l2 d).
Position l (dcons l2 d).
def Subset : Domain -> Domain -> Type.
[A,B]
......@@ -89,10 +83,10 @@ def Subset : Domain -> Domain -> Type.
Position l B.
(; Position and membership ;)
def mem : l : Label -> d : Domain -> Bool.
[ ] mem _ nil --> false
def mem : l : Label -> d : Domain -> bool.
[ ] mem _ dnil --> false
[l1,l2,d]
mem l1 (cons l2 d)
mem l1 (dcons l2 d)
-->
or (label_eq l1 l2)
(mem l1 d).
......@@ -101,7 +95,7 @@ def mem_diff : l1 : Label ->
l2 : Label ->
D : Domain ->
Istrue (not (label_eq l1 l2)) ->
Istrue (mem l1 (cons l2 D)) ->
Istrue (mem l1 (dcons l2 D)) ->
Istrue (mem l1 D).
[l1,l2,D,H1,H12]
mem_diff l1 l2 D H1 H12
......@@ -110,13 +104,13 @@ def mem_diff : l1 : Label ->
def mem_pos : l : Label -> d : Domain -> Istrue (mem l d) -> Position l d.
[l1,l2,d,H]
mem_pos l1 (cons l2 d) H
mem_pos l1 (dcons l2 d) H
-->
dk_string.if_eq_diff
(l : Label => position l1 (cons l d))
(l : Label => position l1 (dcons l d))
l1
l2
(Position_head l1 d)
(Hdiff : Istrue (not (label_eq l2 l1)) =>
(Hdiff : Istrue (not (label_eq l1 l2)) =>
Position_tail l1 l2 d
(mem_pos l1 d (mem_diff l1 l2 d (dk_string.diff_sym l2 l1 Hdiff) H))).
(mem_pos l1 d (mem_diff l1 l2 d Hdiff H))).
......@@ -41,7 +41,7 @@ def eT := pts.eT.
def Pi := pts.Pi.
def Arrow := pts.Arrow.
def Bool := dk_bool.Bool.
def bool := dk_bool.bool.
def true := dk_bool.true.
def false := dk_bool.false.
......@@ -49,28 +49,28 @@ def false := dk_bool.false.
prop : uT.
def Prop : Type := eT prop.
ebP : dk_bool.Bool -> Prop.
ebP : dk_bool.bool -> Prop.
eeP : Prop -> uT.
def eP : Prop -> Type
:= f : Prop => eT (eeP f).
def istrue : Bool -> uT := b : Bool => eeP (ebP b).
def Istrue : Bool -> Type := b : Bool => eP (ebP b).
def istrue : bool -> uT := b : bool => eeP (ebP b).
def Istrue : bool -> Type := b : bool => eP (ebP b).
I : Istrue true.
False_elim : A : uT -> Istrue false -> eT A.
def bool_and_intro : b1 : Bool ->
b2 : Bool ->
def bool_and_intro : b1 : bool ->
b2 : bool ->
Istrue b1 ->
Istrue b2 ->
Istrue (dk_bool.and b1 b2).
[ ]
bool_and_intro dk_bool.true dk_bool.true _ _ --> I.
def bool_and_elim1 : b1 : Bool ->
b2 : Bool ->
def bool_and_elim1 : b1 : bool ->
b2 : bool ->
Istrue (dk_bool.and b1 b2) ->
Istrue b1.
[ ]
......@@ -82,8 +82,8 @@ def bool_and_elim1 : b1 : Bool ->
-->
H.
def bool_and_elim2 : b1 : Bool ->
b2 : Bool ->
def bool_and_elim2 : b1 : bool ->
b2 : bool ->
Istrue (dk_bool.and b1 b2) ->
Istrue b2.
[H]
......@@ -95,8 +95,8 @@ def bool_and_elim2 : b1 : Bool ->
-->
False_elim (istrue b) H.
def bool_or_intro2 : b1 : Bool ->
b2 : Bool ->
def bool_or_intro2 : b1 : bool ->
b2 : bool ->
Istrue b2 ->
Istrue (dk_bool.or b1 b2).
[ ]
......@@ -104,8 +104,8 @@ def bool_or_intro2 : b1 : Bool ->
[H]
bool_or_intro2 dk_bool.false _ H --> H.
def bool_or_elim1 : b1 : Bool ->
b2 : Bool ->
def bool_or_elim1 : b1 : bool ->
b2 : bool ->
Istrue (dk_bool.not b1) ->
Istrue (dk_bool.or b1 b2) ->
Istrue b2.
......@@ -114,8 +114,8 @@ def bool_or_elim1 : b1 : Bool ->
[H12]
bool_or_elim1 dk_bool.false _ _ H12 --> H12.
def not_or_elim : b1 : Bool ->
b2 : Bool ->
def not_or_elim : b1 : bool ->
b2 : bool ->
Istrue (dk_bool.not b1) ->
Istrue (dk_bool.or b1 b2) ->
Istrue b2.
......
#NAME dk_machine_int.
(;
Copyright Raphaël Cauderlier (2014)
<raphael.cauderlier@inria.fr>
This software is a computer program whose purpose is to translate object-oriented program written in the simply-typed ς-calculus from Abadi and Cardelli to Dedukti and Coq.
This software is governed by the CeCILL-B license under French law and
abiding by the rules of distribution of free software. You can use,
modify and/ or redistribute the software under the terms of the CeCILL-B
license as circulated by CEA, CNRS and INRIA at the following URL
"http://www.cecill.info".
As a counterpart to the access to the source code and rights to copy,
modify and redistribute granted by the license, users are provided
only with a limited warranty and the software's author, the holder of
the economic rights, and the successive licensors have only limited
liability.
In this respect, the user's attention is drawn to the risks associated
with loading, using, modifying and/or developing or reproducing the
software by the user in light of its specific status of free software,
that may mean that it is complicated to manipulate, and that also
therefore means that it is reserved for developers and experienced
professionals having in-depth computer knowledge. Users are therefore
encouraged to load and test the software's suitability as regards
their requirements in conditions enabling the security of their
systems and/or data to be ensured and, more generally, to use and
operate it in the same conditions as regards security.
The fact that you are presently reading this means that you have had
knowledge of the CeCILL-B license and that you accept its terms.
;)
def uT := pts.uT.
def eT := pts.eT.
def Bool : Type := dk_bool.Bool.
def UNat : Type := dk_nat.Nat.
def UO : UNat := dk_nat.O.
def US : UNat -> UNat := dk_nat.S.
MInt : UNat -> Type.
O : MInt UO.
S0 : N : UNat -> MInt N -> MInt (US N).
S1 : N : UNat -> MInt N -> MInt (US N).
def zero : N : UNat -> MInt N.
[] zero dk_nat.O --> O
[N] zero (dk_nat.S N) --> S0 N (zero N).
(; equality ;)
def equal : N : UNat -> MInt N -> MInt N -> Bool.
[ ] equal _ O O --> dk_bool.true
[N,n,m]
equal (dk_nat.S N) (S0 _ n) (S0 _ m) --> equal N n m
[N,n,m]
equal (dk_nat.S N) (S1 _ n) (S1 _ m) --> equal N n m
[ ]
equal (dk_nat.S _) (S0 _ _) (S1 _ _) --> dk_bool.false
[ ]
equal (dk_nat.S _) (S1 _ _) (S0 _ _) --> dk_bool.false.
def equal_refl : N : UNat -> n : MInt N -> dk_logic.Istrue (equal N n n).
[ ] equal_refl _ O --> dk_logic.I
[N,n] equal_refl (dk_nat.S N) (S0 _ n) --> equal_refl N n
[N,n] equal_refl (dk_nat.S N) (S1 _ n) --> equal_refl N n.
(; Casting binary natural numbers ;)
def cast_bnat : N : UNat -> bn : dk_binary_nat.BNat -> MInt N.
[N] cast_bnat N dk_binary_nat.O --> zero N
[ ] cast_bnat dk_nat.O _ --> O.
[N,bn]
cast_bnat (dk_nat.S N) (dk_binary_nat.S0 bn)
-->
S0 N (cast_bnat N bn)
[N,bn]
cast_bnat (dk_nat.S N) (dk_binary_nat.S1 bn)
-->
S1 N (cast_bnat N bn).
#NAME dk_binary_nat.
#NAME dk_nat.
(;
......@@ -36,10 +36,24 @@ knowledge of the CeCILL-B license and that you accept its terms.
;)
BNat : Type.
(; Operations ;)
O : BNat.
def S0 : BNat -> BNat.
S1 : BNat -> BNat.
(; twice zero is zero ;)
[] S0 O --> O.
def equal : nat -> nat -> dk_bool.bool.
[] equal 0 0 --> dk_bool.true
[] equal 0 (S _) --> dk_bool.false
[] equal (S _) 0 --> dk_bool.false
[n,m] equal (S n) (S m) --> equal n m.
def equal_refl : n : nat -> dk_logic.Istrue (equal n n).
[] equal_refl 0 --> dk_logic.I
[n] equal_refl (S n) --> equal_refl n.
def eq_rect : n : nat ->
m : nat ->
P : (nat -> pts.uT) ->
dk_logic.Istrue (equal n m) ->
pts.eT (P n) ->
pts.eT (P m).
[x] eq_rect 0 0 _ _ x --> x
[n,m,P,H,x] eq_rect (S n) (S m) P H x --> eq_rect n m (k : nat => P (S k)) H x.
......@@ -44,41 +44,36 @@ def Arrow := pts.Arrow.
(; Have a version of bool independant of cc ;)
(; Booleans ;)
(; booleans ;)
def Bool := dk_bool.Bool.
def true : Bool := dk_bool.true.
def false : Bool := dk_bool.false.
def not : Bool -> Bool := dk_bool.not.
def and : Bool -> Bool -> Bool
def bool := dk_bool.bool.
def true : bool := dk_bool.true.
def false : bool := dk_bool.false.
def not : bool -> bool := dk_bool.not.
def and : bool -> bool -> bool
:= dk_bool.and.
def or :