diff options
| author | Théo Zimmermann | 2019-10-30 17:08:51 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-10-30 17:19:57 +0100 |
| commit | 5d1f7461f74f727d0394e904c3ee820134b22c64 (patch) | |
| tree | f6994531881fce585e6915e23498e194aadc5ad4 | |
| parent | 201f31d3cdb1cd30646a622ec4b46d7cbcb24e20 (diff) | |
Use explicit match as suggested by Clément.
| -rw-r--r-- | doc/sphinx/language/cic.rst | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index ef896b6f03..9e4210793e 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1067,7 +1067,8 @@ between universes for inductive types in the Type hierarchy. .. coqtop:: all - Definition I_not_I '(not_I_I not_I : I) : ~ I := not_I. + Definition I_not_I : I -> ~ I := fun i => + match i with not_I_I not_I => not_I end. .. coqtop:: in |