mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-10-26 16:58:48 +03:00
correct 'inductivelly' typo
This commit is contained in:
parent
c64d343051
commit
b20b0e6c7b
@ -38,7 +38,7 @@ Main : IO (Result () String) {
|
|||||||
}
|
}
|
||||||
```
|
```
|
||||||
|
|
||||||
Theorems can be proved inductivelly, as in [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php) and [Idris](https://www.idris-lang.org/):
|
Theorems can be proved inductively, as in [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php) and [Idris](https://www.idris-lang.org/):
|
||||||
|
|
||||||
```javascript
|
```javascript
|
||||||
// Black Friday Theorem. Proof that, for every Nat n: n * 2 / 2 == n.
|
// Black Friday Theorem. Proof that, for every Nat n: n * 2 / 2 == n.
|
||||||
|
Loading…
Reference in New Issue
Block a user