Variable mkTyVar : Name -> Kind -> CoreVar.
Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
- Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
+ Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoType t1 t2))".
Variable mkExVar : Name -> CoreType -> CoreVar.
Extract Inlined Constant mkExVar => "Id.mkLocalId".
(hetmet_pga_applyr : CoreVar)
(hetmet_pga_curryl : CoreVar)
(hetmet_pga_curryr : CoreVar)
+ (hetmet_pga_loopl : CoreVar)
+ (hetmet_pga_loopr : CoreVar)
.
(* ; ga_curry := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
(* ; ga_apply := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
(* ; ga_kappa := fun Γ Δ ec l a => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)
+ ; ga_loopl := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_loopl (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x))
+ ; ga_loopr := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_loopr (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x))
; ga_lit := fun Γ Δ ec l a => Prelude_error "ga_lit"
; ga_curry := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
; ga_apply := fun Γ Δ ec l a b c => Prelude_error "ga_apply"
(hetmet_pga_applyl : CoreVar)
(hetmet_pga_applyr : CoreVar)
(hetmet_pga_curryl : CoreVar)
- (hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) :=
+ (hetmet_pga_curryr : CoreVar)
+ (hetmet_pga_loopl : CoreVar)
+ (hetmet_pga_loopr : CoreVar)
+ : list (@CoreBind CoreVar) :=
coqPassCoreToCore'
do_flatten
do_skolemize
hetmet_pga_copy
hetmet_pga_drop
hetmet_pga_swap
+ hetmet_pga_loopl
+ hetmet_pga_loopr
lbinds
(*
hetmet_pga_applyl