diff options
| author | Arnaud Spiwack | 2015-06-24 14:45:41 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-06-24 17:55:47 +0200 |
| commit | ec74137b4e4b96135c43570b5f149e7e1ec0db9c (patch) | |
| tree | cca6c92be1c44fef09c148ac99638ec232ffd33f /kernel/typeops.ml | |
| parent | 2adff76c5466734c633923e768c9dcbdc6f28c86 (diff) | |
Add syntax entry to assume strict positivity of an inductive type.
The syntax is `Assume [Positive]` Inductive/CoInductive/Record…`. The square brackets are used to delimit what is actually a list, so that other such flags can be passed in the future (universes, guard condition…).
Diffstat (limited to 'kernel/typeops.ml')
0 files changed, 0 insertions, 0 deletions