...
 
Commits (2)
......@@ -19,7 +19,7 @@ theory NatManually : ur:?DHOL =
p_s: p_n ⟶ p_n ❘ = [f][x] s (f x) ❙
p_induct_n: n ⟶ p_n ❘ = induct_n p_n p_z p_s ❙
p_induct_z: DED (induct_n p_n p_z p_s z) EQ p_z ❘ = induct_z p_n p_z p_s
p_induct_z: DED (induct_n p_n p_z p_s z) EQ p_z ❘ = induct_z ❙
p_induct_s: {X:n} DED (induct_n p_n p_z p_s (s X)) EQ p_s (induct_n p_n p_z p_s X) ❘
= [X] induct_s X ❙
......@@ -30,26 +30,34 @@ theory NatManually : ur:?DHOL =
theory NatExample : ?LFXI =
theory nat_decls_long =
n: type ❙
z: n ❙
s: n ⟶ n ❙
reflect nat_long() : NatExample/nat_decls_long() ❙
inductive_definition plusn_long() : nat_long() ❘ =
n = nat_long/n ⟶ nat_long/n ❙
z: n ❘ = ([x] x) ❙
s: n ⟶ n ❘ = ([u,x] nat_long/s (u x)) ❙
theory unital_type =
n: type ❙
z: n ❙
theory nat_decls =
include ?NatExample/unital_type ❙
s: n ⟶ n ❙
reflect nat() : NatExample/nat_decls() ❙
inductive nats() ❘ =
n: type ❙
z: n ❙
s: n ⟶ n ❙
inductive_definition plusn() : nat() ❘ =
n: type ❘ = (nat/n ⟶ nat/n)
n = nat/n ⟶ nat/n
z: n ❘ = ([x] x) ❙
s: n ⟶ n ❘ = ([u,x] nat/s (u x)) ❙
......@@ -63,7 +71,7 @@ theory NatExample : ?LFXI =
ind_proof z_right_neutral() : nat() ❘=
n = [m] DED m EQ (m + nat/z) ❙
z = plusn/z/Applied nat/z
z = SYM (plusn/z/Applied nat/z)
s : {x:nat/n} n x ⟶ n (nat/s x) ❘ = [x, px] (px CONG nat/s) TRANS (SYM (plusn/s/Applied x nat/z)) ❙
......