|
|
fd2c035902
|
work on soundness proofs & fix bug in translate_typing
|
2024-09-19 07:02:27 +02:00 |
|
|
|
826077e37b
|
coq: add translate_typing example
& other minor stuff
|
2024-09-19 01:46:29 +02:00 |
|
|
|
6e5c832db7
|
add notation for sequence types & use notations everywhere
|
2024-09-18 11:15:20 +02:00 |
|
|
|
f53f226f55
|
remove module wraps in each file
|
2024-09-17 03:13:36 +02:00 |
|
|
|
12da3e97bd
|
change meaning of expr_ascend to only explicitly state the top segment of the type ladder.
also add associativity of ladder types in type-equivalence
|
2024-09-16 15:58:29 +02:00 |
|
|
|
638ddf4fd1
|
coq: add translate_typing
|
2024-09-08 15:34:15 +02:00 |
|
|
|
10ca08c5a0
|
coq typing relation: add DescendImplicit rule in addition to Descend rule for explicit type-downcasts
add one more typing example
|
2024-09-08 15:33:54 +02:00 |
|
|
|
4b3358372e
|
coq: typing relation fix ctx assignments in premisse
|
2024-09-08 15:32:54 +02:00 |
|
|
|
bf7846294f
|
coq: move context into separate module, define morphism-path & redefine typing rules
|
2024-09-05 12:47:30 +02:00 |
|
|
|
75fab989d7
|
work on typing rules
|
2024-09-04 12:39:15 +02:00 |
|
|
|
b978637b57
|
coq: change notation brackets for terms
|
2024-08-22 09:57:47 +02:00 |
|
|
|
4323e7d09f
|
coq: add another typing example
|
2024-08-22 08:31:14 +02:00 |
|
|
|
ad107759bf
|
coq: expr alpha conversion
|
2024-08-22 08:30:46 +02:00 |
|
|
|
39f312b401
|
coq: rename expr_term constructors: remove 'tm' prefix
|
2024-08-22 08:19:48 +02:00 |
|
|
|
61f1234fcc
|
coq: add 'compatible' typing relation
|
2024-08-21 20:04:20 +02:00 |
|
|
|
3a84dada65
|
coq notation definition for expressions
|
2024-08-18 10:28:56 +02:00 |
|
|
|
eebb096f8a
|
coq: wip typing
|
2024-07-27 13:30:12 +02:00 |
|
|
|
292234c247
|
rename term types to expr_term and type_term and type_abs->type_univ, type_app->type_spec
|
2024-07-25 12:40:12 +02:00 |
|
|
|
d8200b56b4
|
coq: preliminary definition of typing-relation
|
2024-07-24 11:22:39 +02:00 |
|
