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

coq: add morphism type

Browse source
This commit is contained in:
Michael Sippel 2024-07-25 12:41:44 +02:00
parent 292234c247
commit ec955c3c19
Signed by: senvas
GPG key ID: F96CF119C34B64A6
2 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
coq/subst.v
View file

@ -23,6 +23,7 @@ Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=
| expr_ty_abs x e => if (eqb v x) then e0 else expr_ty_abs x (expr_subst v n e)
| expr_ty_app e t => expr_ty_app (expr_subst v n e) t
| expr_tm_abs x t e => if (eqb v x) then e0 else expr_tm_abs x t (expr_subst v n e)
| expr_tm_abs_morph x t e => if (eqb v x) then e0 else expr_tm_abs_morph x t (expr_subst v n e)
| expr_tm_app e a => expr_tm_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_ascend t e => expr_ascend t (expr_subst v n e)

2
coq/terms.v
View file

@ -15,6 +15,7 @@ Inductive type_term : Type :=
| type_fun : type_term -> type_term -> type_term
| type_univ : string -> type_term -> type_term
| type_spec : type_term -> type_term -> type_term
| type_morph : type_term -> type_term -> type_term
| type_ladder : type_term -> type_term -> type_term
.
@ -24,6 +25,7 @@ Inductive expr_term : Type :=
| expr_ty_abs : string -> expr_term -> expr_term
| expr_ty_app : expr_term -> type_term -> expr_term
| expr_tm_abs : string -> type_term -> expr_term -> expr_term
| expr_tm_abs_morph : string -> type_term -> expr_term -> expr_term
| expr_tm_app : expr_term -> expr_term -> expr_term
| expr_let : string -> type_term -> expr_term -> expr_term -> expr_term
| expr_ascend : type_term -> expr_term -> expr_term