From c49e080cc3f095a0f9ccca1f92a29e68c8fb11d0 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sat, 17 Sep 2022 21:46:43 +0200 Subject: [PATCH] typos --- posts/2022-09-16-ats.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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