18 commits

Author	SHA1	Message	Date
Adam Chlipala	ac0a15e9f2	Rename typing relations from hasty to has_ty	2023-03-19 11:59:34 -04:00
Adam Chlipala	c5a69b6253	Revising for tomorrow's lecture	2022-03-13 18:10:19 -04:00
Adam Chlipala	f5aed26c77	LambdaCalculusAndTypeSoundness: remove the other use of evaluation contexts	2021-03-27 18:57:03 -04:00
Adam Chlipala	5cdd4d1322	Start of splitting evaluation contexts out of LambdaCalculusAndTypeSoundness	2021-03-27 17:03:26 -04:00
Adam Chlipala	d3c7a85b49	More cleanup around addition of RuleInduction	2021-03-01 12:15:34 -05:00
Adam Chlipala	4388ecc80e	Revising LambdaCalculusAndTypeSoundness	2018-04-01 13:06:47 -04:00
Adam Chlipala	2832696faa	Start of CompilerCorrectness: cfoldExprs_ok	2017-03-18 14:42:13 -04:00
Adam Chlipala	b27e58f11e	Bump chapter numbers in Coq code comments	2017-02-21 09:00:30 -05:00
Adam Chlipala	0e68042f07	Fix for Coq 8.5 again	2017-02-07 21:35:23 -05:00
Adam Chlipala	1768aa6ea7	Progress on porting to Coq 8.6	2017-02-07 18:51:05 -05:00
Adam Chlipala	0fe16514a4	Change some tactics to use their usual names in the book code	2016-03-13 21:15:03 -04:00
Adam Chlipala	8f0c986a00	Finished LambdaCalculus chapter	2016-03-13 21:11:51 -04:00
Adam Chlipala	b3692b97a5	LambdaCalculus chapter: a nonterminating lambda term	2016-03-13 19:52:46 -04:00
Adam Chlipala	ec261d542c	Comment LambdaCalculusAndTypeSoundness	2016-03-13 15:17:09 -04:00
Adam Chlipala	a36ebc7802	LambdaCalculusAndTypeSoundness: Church numerals	2016-03-13 14:44:41 -04:00
Adam Chlipala	55257f669d	LambdaCalculusAndTypeSoundness: untyped lambda calculus semantics, two ways	2016-03-13 13:47:25 -04:00
Adam Chlipala	9ce653261c	LambdaCalculusAndTypeSoundness: a more manual soundness proof	2016-03-13 11:54:38 -04:00
Adam Chlipala	23955eb536	Start LambdaCalculusAndTypeSoundness: automated soundness proof	2016-03-13 11:34:06 -04:00