pass on the checker

CoqHott · Jan 4, 2024 · 3b1f853 · 3b1f853
1 parent 622f577
commit 3b1f853
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/theories/Readme.v b/theories/Readme.v
@@ -404,6 +404,14 @@ Import IndexedDefinitions.
 
 From LogRel.Decidability Require Import Functions.
 
+(* The main innovation: the function which compacts a to-be neutral once the reduction machine
+has hit a variable *)
+
+About compact.
+
+(* The other functions for conversion and typing, are only extended with the new cases
+  related to lists *)
+
 About conv.
 About typing.