rhi/blog
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

typos

Browse source
This commit is contained in:
rhiannon morris 2022-09-17 21:46:43 +02:00
parent 0ec38537f4
commit c49e080cc3
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
posts/2022-09-16-ats.md
View file

@ -181,9 +181,9 @@ typedef term(n : int) = [h : nat] term(n, h)
a variable is [a de bruijn index][db], which is a natural less than `n`. to a variable is [a de bruijn index][db], which is a natural less than `n`. to
express this we need to bridge the static world, where `n` lives, and the express this we need to bridge the static world, where `n` lives, and the
dynamic, where `Var`'s field lives. to do this i use a singleton type dynamic, where `Var`'s field lives. so i'm using a singleton type `int(i)`,
`int(i)`, whose only value is `i` itself. with this type, you can constraint the whose only value is `i` itself. with this type, you can constrain the static
static `i`, and in turn the value of the field. `i`, and in turn the value of the field.
[db]: https://en.wikipedia.org/wiki/De_Bruijn_index [db]: https://en.wikipedia.org/wiki/De_Bruijn_index