§ Boolean Reflection Design

• To decide some kind of property involving free variables, we split it into two parts:
• First, closed term that interns all free variables into an AST (makes them into bvars), so we have e.g. decidable equality on it, which is closed.
• An environment that refers to the local context (i.e. the fvars), which needs to be built by metaprogramming.
• So, for example, to implement something like ring, we have a part that uses bvars to be able to build closed terms, and a decidable "isomorphism" predicate which shows that they will be equal.