Michael Sippel fd2c035902 work on soundness proofs & fix bug in translate_typing		2024-09-19 07:02:27 +02:00
..
_CoqProject	add initial impl of debruijn terms	2024-09-19 01:48:12 +02:00
bbencode.v	add notation for sequence types & use notations everywhere	2024-09-18 11:15:20 +02:00
context.v	remove module wraps in each file	2024-09-17 03:13:36 +02:00
equiv.v	coq: type equiv: add subfun/submorph	2024-09-19 01:41:51 +02:00
morph.v	add notation for sequence types & use notations everywhere	2024-09-18 11:15:20 +02:00
smallstep.v	add notation for sequence types & use notations everywhere	2024-09-18 11:15:20 +02:00
soundness.v	work on soundness proofs & fix bug in translate_typing	2024-09-19 07:02:27 +02:00
subst.v	coq: add translate_typing example	2024-09-19 01:46:29 +02:00
subtype.v	remove module wraps in each file	2024-09-17 03:13:36 +02:00
terms.v	add notation for sequence types & use notations everywhere	2024-09-18 11:15:20 +02:00
terms_debruijn.v	add initial impl of debruijn terms	2024-09-19 01:48:12 +02:00
typing.v	work on soundness proofs & fix bug in translate_typing	2024-09-19 07:02:27 +02:00