Commit ae02d3c0 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

typo

parent 70551b7b
......@@ -49,7 +49,7 @@ Inductive t :=
The `Cᵢ` are *constructors* of type `t`, they may require some arguments (or not), but anyway they always have `t` as result type (after the rightmots arrow).
In fact, `t` itselft may have arguments, turning it into an *inductive type scheme* (we also say *inductive predicate*). We'll see examples of that later.
In fact, `t` itself may have arguments, turning it into an *inductive type scheme* (we also say *inductive predicate*). We'll see examples of that later.
Basic examples (already in the Coq standard library, no need to copy-paste them).
......@@ -175,6 +175,8 @@ Fixpoint pow n : Type :=
end.
```
### The option type
```coq
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment