• First, consider an AST for natural numbers, which keeps track of the number of variables a n : Nat. We use Fin n to represent variables, and thus our environments exactly correspond to the number of variables.

namespace Natinductive NatExpr (n : Nat) : Type| var : (v : Fin n) → NatExpr n| add : NatExpr n → NatExpr n → NatExpr ndef NatExpr.eval (e : NatExpr n) (env : Fin n → Nat) : Nat :=  match e with  | .var v => env v  | .add e1 e2 => NatExpr.eval e1 env + NatExpr.eval e2 envinductive NatPredicate (n : Nat) : Type| eq : NatExpr n → NatExpr n → NatPredicate ndef NatPredicate.eval (env : Fin n → Nat) : NatPredicate n → Prop  | .eq e1 e2 => NatExpr.eval e1 env = NatExpr.eval e2 envdef NatPredicate.decide : NatPredicate n → Bool := sorrytheorem NatPredicate.decide_iff_eval (p : NatPredicate n) :  (∀ (env : Fin n → Nat), p.eval env) ↔  (p.decide = true) := sorryend Nat

• Now, we want to do the same with bitvectors. How does this work?

namespace BVopen Natabbrev BVTyCtx (natCard : Nat) (bvCard : Nat) : Type :=  Fin bvCard → NatExpr natCardinductive BVExpr (ctx : BVTyCtx natCard bvCard) : (NatExpr natCard) → Type| var (v : Fin bvCard) : BVExpr ctx (ctx v)| add (a : BVExpr ctx w) (b : BVExpr ctx w) : BVExpr ctx w| append (a : BVExpr ctx v) (b : BVExpr ctx w) : BVExpr ctx (.add v w)abbrev BVEnv (tyCtx : BVTyCtx natCard bvCard) (natEnv : Fin natCard → Nat) :=  (v : Fin bvCard) → BitVec ((tyCtx v).eval natEnv)def BVExpr.eval {natEnv : Fin n → Nat} (bvEnv : BVEnv bvCard natEnv) :  BVExpr bvCard w → BitVec (w.eval natEnv)| .var v => bvEnv v| .add a b => a.eval bvEnv + b.eval bvEnv| .append a b => a.eval bvEnv ++ b.eval bvEnvend BV

• What's the general algorithm here? Given typing rules, how does one write down the corresponding intrinsically well-typed AST?