diff options
| -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 |