|
|
63b121a815
|
add inversion lemmas (without proof)
|
2024-09-24 05:32:59 +02:00 |
|
|
|
48429c6316
|
add preliminary proof of transl_preservation (with env_wf Γ admitted)
|
2024-09-24 04:59:58 +02:00 |
|
|
|
ac63139c67
|
add preconditions of expr_lc in eval; use coinductive quantification in T_TypeAbs
|
2024-09-24 04:42:45 +02:00 |
|
|
|
f0d9a550b6
|
prove typing preservation of morphism translation
|
2024-09-24 04:42:45 +02:00 |
|
|
|
a5d8cb979b
|
rename context to env
|
2024-09-24 04:42:45 +02:00 |
|
|
|
cc96cee283
|
add environment library to metatheory
|
2024-09-24 04:41:56 +02:00 |
|
|
|
d690d6dcdc
|
organize coq sources in subdirectories
|
2024-09-21 13:00:57 +02:00 |
|
|
|
f8effc45ad
|
add evaluation for debruijn terms
|
2024-09-21 00:41:45 +02:00 |
|
|
|
1edbb8d748
|
add context, morphism translation & typing for debruijn terms
|
2024-09-21 00:41:45 +02:00 |
|
|
|
f76cec4a9d
|
add subtype relations for debruijn terms
|
2024-09-21 00:41:45 +02:00 |
|
|
|
1d6fb9ab6d
|
add equivalence relation for debruijn types
|
2024-09-21 00:41:45 +02:00 |
|
|
|
c4f4e56fee
|
move subst/opening lemmas to separate file
|
2024-09-21 00:41:45 +02:00 |
|
|
|
9264d28837
|
take over Metatheory, FiniteSet & Atom libraries from popl-tutorial
|
2024-09-21 00:41:40 +02:00 |
|
|
|
dbfe0cf4de
|
add initial impl of debruijn terms
|
2024-09-19 01:48:12 +02:00 |
|
|
|
bf7846294f
|
coq: move context into separate module, define morphism-path & redefine typing rules
|
2024-09-05 12:47:30 +02:00 |
|
|
|
b31c8abc6c
|
initial definition of soundness theorems
|
2024-09-04 12:41:17 +02:00 |
|
|
|
2db774ae68
|
initial definition of expand_morphisms
|
2024-09-04 12:41:00 +02:00 |
|
|
|
42ae93f2d7
|
coq: add subtype relations
|
2024-08-21 15:02:43 +02:00 |
|
|
|
61948c6dc6
|
setup coq project & initial definition of terms (types & expressions)
|
2024-07-24 11:22:25 +02:00 |
|
