Merge pull request #527 from NaoEhSavio/main

replace data with type
This commit is contained in:
Nicolas Abril 2024-05-29 15:08:44 +00:00 committed by GitHub
commit 523300bd4c
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
3 changed files with 7 additions and 7 deletions

View File

@ -5,7 +5,7 @@
## String
```python
data String = (Cons head ~tail) | (Nil)
type String = (Cons head ~tail) | (Nil)
```
@ -23,7 +23,7 @@ A String literal is surrounded with `"`. Accepts the same values as characters l
## List
```python
data List = (Cons head ~tail) | (Nil)
type List = (Cons head ~tail) | (Nil)
```
- **Nil**: Represents an empty list.
@ -41,7 +41,7 @@ A List of values can be written using `[ ]`, it can have multiple values inside,
## Nat
```python
data Nat = (Succ ~pred) | (Zero)
type Nat = (Succ ~pred) | (Zero)
```
- **Succ ~pred**: Represents a natural number successor.
- **Zero**: Represents the natural number zero.
@ -57,7 +57,7 @@ A Natural Number can be written with literals with a `#` before the literal numb
## Result
```python
data Result = (Ok val) | (Err val)
type Result = (Ok val) | (Err val)
```
- **Ok val**: Represents a successful result with value `val`.
@ -65,7 +65,7 @@ data Result = (Ok val) | (Err val)
## Map
```python
data Map = (Node value ~left ~right) | (Leaf)
type Map = (Node value ~left ~right) | (Leaf)
```
- **Node value ~left ~right**: Represents a map node with a `value` and `left` and `right` subtrees.

View File

@ -153,7 +153,7 @@ impl<'a> TermParser<'a> {
}
fn parse_datatype(&mut self, builtin: bool) -> ParseResult<(Name, Adt)> {
// data name = ctr (| ctr)*
// type name = ctr (| ctr)*
self.skip_trivia();
let name = self.labelled(|p| p.parse_top_level_name(), "datatype name")?;
self.consume("=")?;

View File

@ -1,4 +1,4 @@
# data Tree = (Leaf x) | (Node x0 x1)
# type Tree = (Leaf x) | (Node x0 x1)
Leaf = λx λl λn (l x)
Node = λx0 λx1 λl λn (n x0 x1)