senvas/ladder-calculus
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

expr term: remove explicit variable-type from expr_let

Browse source
This commit is contained in:
Michael Sippel 2024-09-08 14:48:36 +02:00
parent bf7846294f
commit c3d1649402
Signed by: senvas
GPG key ID: F96CF119C34B64A6
3 changed files with 4 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
coq/bbencode.v
View file

@ -55,13 +55,8 @@ Definition bb_succ : expr_term :=
(expr_var "z")))))))).
Definition e1 : expr_term :=
(expr_let "bb-zero" (type_ladder (type_id "ℕ")
(type_ladder (type_id "BBNat")
(type_univ "α"
(type_fun (type_fun (type_var "α") (type_var "α"))
(type_fun (type_var "α") (type_var "α"))))))
bb_zero
(expr_app (expr_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
(expr_let "bb-zero" bb_zero
(expr_app (expr_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
).
Definition t1 : expr_term := (expr_app (expr_var "x") (expr_var "x")).

2
coq/subst.v
View file

@ -115,7 +115,7 @@ Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=
| expr_abs x t e => if (eqb v x) then e0 else expr_abs x t (expr_subst v n e)
| expr_morph x t e => if (eqb v x) then e0 else expr_morph x t (expr_subst v n e)
| expr_app e a => expr_app (expr_subst v n e) (expr_subst v n a)
| expr_let x t a e => expr_let x t (expr_subst v n a) (expr_subst v n e)
| expr_let x a e => expr_let x (expr_subst v n a) (expr_subst v n e)
| expr_ascend t e => expr_ascend t (expr_subst v n e)
| expr_descend t e => expr_descend t (expr_subst v n e)
end.

3
coq/terms.v
View file

@ -25,12 +25,11 @@ Inductive expr_term : Type :=
| expr_abs : string -> type_term -> expr_term -> expr_term
| expr_morph : string -> type_term -> expr_term -> expr_term
| expr_app : expr_term -> expr_term -> expr_term
| expr_let : string -> type_term -> expr_term -> expr_term -> expr_term
| expr_let : string -> expr_term -> expr_term -> expr_term
| expr_ascend : type_term -> expr_term -> expr_term
| expr_descend : type_term -> expr_term -> expr_term
.
(* TODO
Inductive type_DeBruijn : Type :=