Wen Kokke f04dbd2c65 Updated Lambda to specify determinism implies the diamond property and confluence, but the diamond property does not imply confluence by itself.e		2020-07-13 15:03:00 +01:00
..
denotational	moving denotational back to plfa, updates to Confluence	2019-05-25 16:11:01 -04:00
extra	Make sum type right-associative	2019-12-02 09:49:49 +02:00
fresh	restoring extra	2019-01-08 14:11:20 +00:00
qtt	Quantitative: fixes a spelling error	2019-06-20 14:00:41 +02:00
stlc	Lambda: fixes spellings of a few words	2019-01-25 23:31:10 +00:00
842Inference.agda	Added rewrite of Inference by Prabhakar	2020-05-22 15:50:50 +01:00
bin-suggestion.lagda.md	added Levy suggestion to extra	2020-04-30 08:36:48 -03:00
broken.lagda	restoring extra	2019-01-08 14:11:20 +00:00
Inherent.lagda	restoring extra	2019-01-08 14:11:20 +00:00
iso-exercise.lagda	added Levy suggestion to extra	2020-04-30 08:36:48 -03:00
Issue488.agda	Updated Lambda to specify determinism implies the diamond property and confluence, but the diamond property does not imply confluence by itself.e	2020-07-13 15:03:00 +01:00
KovacsSTLCnorm.agda	Added Kovacs strong normalisation proof to extra	2019-01-22 15:33:12 +00:00
LambdaReduction.lagda.md	Restructured directory.	2019-08-15 17:26:21 +01:00
Modules.lagda.md	Restructured directory.	2019-08-15 17:26:21 +01:00
plfa-extra.agda-lib	making progress towards qtt/more	2019-03-10 20:20:20 +01:00
Pure.lagda	restoring extra	2019-01-08 14:11:20 +00:00
PureConor.lagda	restoring extra	2019-01-08 14:11:20 +00:00
Raw.lagda	restoring extra	2019-01-08 14:11:20 +00:00
Reflection.lagda.md	Restructured directory.	2019-08-15 17:26:21 +01:00