- (* the CoreVar for the "magic" bracket/escape identifiers must be created from within one of the monads *)
- Context (hetmet_brak_var : CoreVar).
- Context (hetmet_esc_var : CoreVar).
-
- Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
- fun _ => trustMeCoercion.
-
- Fixpoint weakExprToCoreExpr (f:Fresh unit (fun _ => WeakExprVar)) (me:WeakExpr) : @CoreExpr CoreVar :=