diff --git a/posts/2022-09-16-ats.md b/posts/2022-09-16-ats.md index 9de512b..f98e4d7 100644 --- a/posts/2022-09-16-ats.md +++ b/posts/2022-09-16-ats.md @@ -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 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 -`int(i)`, whose only value is `i` itself. with this type, you can constraint the -static `i`, and in turn the value of the field. +dynamic, where `Var`'s field lives. so i'm using a singleton type `int(i)`, +whose only value is `i` itself. with this type, you can constrain the static +`i`, and in turn the value of the field. [db]: https://en.wikipedia.org/wiki/De_Bruijn_index