Merge pull request #11 from TheoWinterhalter/discr

Discrimination of erased natural numbers
TheoWinterhalter · May 28, 2024 · 873af06 · 873af06
2 parents b29a2ec + 98ba3cd
commit 873af06
Show file tree

Hide file tree

Showing 3 changed files with 679 additions and 0 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -32,6 +32,7 @@ theories/Model.v
 theories/Admissible.v
 
 theories/FreeTheorem.v
+theories/Examples.v
 
 theories/RTyping.v
 theories/Potential.v

diff --git a/doc/index.md b/doc/index.md
@@ -67,13 +67,15 @@ Autosubst library and some notations.
 | [Model]       | Consequences of the model                                     |
 | [Admissible]  | Simpler typing rules for GTT, assuming injectivity of Π-types |
 | [FreeTheorem] | Proof-of-concept free theorem for GTT                         |
+| [Examples]    | Examples from the paper                                       |
 
 [Erasure]: coqdoc/GhostTT.Erasure.html
 [Revival]: coqdoc/GhostTT.Revival.html
 [Param]: coqdoc/GhostTT.Param.html
 [Model]: coqdoc/GhostTT.Model.html
 [Admissible]: coqdoc/GhostTT.Admissible.html
 [FreeTheorem]: coqdoc/GhostTT.FreeTheorem.html
+[Examples]: coqdoc/GhostTT.Examples.html
 
 ### GRTT (theory with reflection of equality)