File tree Expand file tree Collapse file tree 1 file changed +5
-7
lines changed Expand file tree Collapse file tree 1 file changed +5
-7
lines changed Original file line number Diff line number Diff line change @@ -407,6 +407,7 @@ follows:
407
407
```
408
408
409
409
The clauses of this definition can be read :
410
+
410
411
- \idr{Z} is a natural number .
411
412
- \idr{S} is a "constructor" that takes a natural number and yields another one
412
413
-- that is , if \idr{n} is a natural number , then \idr{S n } is too .
@@ -796,14 +797,11 @@ we believe will be useful for making some larger argument, use holes to delay
796
797
defining them for the moment, and continue working on the main argument until we
797
798
are sure it makes sense; then we can go back and fill in the proofs we skipped .
798
799
799
- \todo[inline]{
800
- Decide whether or not to discuss \idr{postulate}.
800
+ \todo[inline]{Decide whether to discuss \idr{postulate}.}
801
801
802
- ```idris
803
- -- Be careful , though: every time you say `postulate` you are leaving a door open
804
- -- for total nonsense to enter Idris's nice, rigorous, formally checked world!
805
- ```
806
- }
802
+ > -- Be careful , though: every time you say `postulate` you are leaving a door
803
+ > -- open for total nonsense to enter Idris's nice , rigorous, formally checked
804
+ > -- world!
807
805
808
806
We can also use the \idr{rewrite} tactic with a previously proved theorem
809
807
instead of a hypothesis from the context. If the statement of the previously
You can’t perform that action at this time.
0 commit comments