| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-08-31 | Numeral Notation (for inductive types) | Pierre Letouzey | |
| This is a portion of roglo's PR#156 introducing a Numeral Notation command : we deal here with inductive types via conversion fonctions from/to Z written in Coq. For an example, see plugins/syntax/NatSyntaxViaZ.v This commit does not include the part about printing via some ltac. Using ltac was meant for dealing with real numbers, let's see first what become PR#415 about a compact representation for real literals. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |