Skip to content

Commit

Permalink
Tiny fix in docs
Browse files Browse the repository at this point in the history
  • Loading branch information
fizruk committed Jun 30, 2023
1 parent 07b520a commit 7cc7f38
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion docs/docs/reference/builtins/unit.rzk.md
Expand Up @@ -7,7 +7,7 @@ Since [:octicons-tag-24: v0.5.1][Unit support]
```

In the syntax, only `Unit` (the type) and `unit` (the only inhabitant) are provided. Everything else should be available from computation rules.
More specifically, `rzk` takes the uniqueness property of the `Unit` type (see Section 1.5 of the HoTT book[^1]) as the computation rule, meaning that any (well-typed) term of type Unit reduces to unit.
More specifically, `rzk` takes the uniqueness property of the `Unit` type (see Section 1.5 of the HoTT book[^1]) as the computation rule, meaning that any (well-typed) term of type `Unit` reduces to `unit`.
This means in particular, that induction and uniqueness can be defined very easily:

```rzk
Expand Down

0 comments on commit 7cc7f38

Please sign in to comment.