|
|
d31101103f
|
coq: add expr_fv_type
|
2024-09-24 12:08:00 +02:00 |
|
|
|
666d14e91d
|
add #[export] to all Hints
|
2024-09-24 08:49:20 +02:00 |
|
|
|
ac63139c67
|
add preconditions of expr_lc in eval; use coinductive quantification in T_TypeAbs
|
2024-09-24 04:42:45 +02:00 |
|
|
|
10cd2f9bc9
|
fix expr_open & expr_lc for let case
|
2024-09-24 04:42:45 +02:00 |
|
|
|
4fde2442f1
|
fix naming of rules in expr_lc
|
2024-09-24 04:42:45 +02:00 |
|
|
|
a5d8cb979b
|
rename context to env
|
2024-09-24 04:42:45 +02:00 |
|
|
|
d690d6dcdc
|
organize coq sources in subdirectories
|
2024-09-21 13:00:57 +02:00 |
|
