-Definition weakVarToCoreVar (wv:WeakVar) : CoreVar :=
-match wv with
-| WExprVar (weakExprVar v _ ) => v
-| WTypeVar (weakTypeVar v _ ) => v
-| WCoerVar (weakCoerVar v _ _ ) => v
-end.
-Coercion weakVarToCoreVar : WeakVar >-> CoreVar.
-
-Section HaskWeakToCore.
-
- (* 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 _ => unsafeCoerce.