fact: Definition reify_helper {var : Type} (term : nat) (ctx : @var_context.var_context var) : M (@expr var) := ((mfix2 reify_helper (term : nat) (ctx : @var_context.var_context var) : M (@expr var) := lvar <- find_in_ctx term ctx; match lvar with | Some v => M.ret (@Var var v) | None => mmatch term with | [#] O | =n> M.ret (@NatO var) | [#] S | x =n> rx <- reify_helper x ctx; M.ret (@NatS var rx) | [#] Nat.mul | x y =n> rx <- reify_helper x ctx; ry <- reify_helper y ctx; M.ret (@NatMul var rx ry) | [#] @Let_In nat (fun _=>nat) | v f =n> rv <- reify_helper v ctx; rf <- (M.nu (FreshFrom f) mNone (fun x : nat => M.nu Generate mNone (fun vx : var => let fx := reduce (RedWhd [rl:RedBeta]) (f x) in rf <- reify_helper fx (var_context.cons x vx ctx); M.abs_fun vx rf))); M.ret (@LetIn var rv rf) end end) term ctx).
imports: Coq.ZArith.ZArith Coq.Lists.List