Ptival
/ .gitignore
Last active
October 28, 2021 10:40
Accompanying code for https://ptival.github.io/deep-dive-meta-theory-carte-3 (NOTE: there should be a "Download ZIP" button in the top-right corner)
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| *.aux | |
| *.glob | |
| *.vo | |
| *.vok | |
| *.vos | |
| .envrc | |
| .Makefile.coq.d | |
| Makefile.coq | |
| Makefile.coq.conf |
Ptival
/ mtc-2.v
Last active
February 18, 2020 14:06
Accompanying code for https://ptival.github.io/deep-dive-meta-theory-carte-2
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (** Preliminary definitions *) | |
| Class SupportsFeature (E F : Set -> Set) := | |
| { | |
| inject : forall (A : Set), F A -> E A; | |
| }. | |
| Arguments inject {E F _ A}. | |
| Notation "E 'supports' F" := (SupportsFeature E F) (at level 50). | |
| Global Instance supports_Refl F |
Ptival
/ mtc-1.v
Created
January 31, 2020 00:03
Accompanying code for https://ptival.github.io/deep-dive-meta-theory-carte-1
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (** Our two extensible language feature definitions *) | |
| Inductive Boolean (E : Set) : Set := | |
| | MkBoolean (b : bool) | |
| | IfThenElse (condition thenBranch elseBranch : E) | |
| . | |
| Arguments MkBoolean {E}. | |
| Arguments IfThenElse {E}. | |
| Inductive Natural (E : Set) : Set := |