...

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)) ❙ ❚ ... ...