- (* a ExprCaseBranch contains all the data found in a case branch except the expression itself *)
- Record ExprCaseBranch {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} :=
- { cbi_sacic : @StrongAltConInContext n tc Γ atypes
- ; cbi_vars : vec VV (tagNumValVars (cbi_tag cbi_sacic))
- ; cbi_varstypes := vec2list (vec_zip cbi_vars (cbi_types cbi_sacic))
+ (* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *)
+
+ Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)} :=
+ { scbwv_sac : @StrongAltCon tc
+ ; scbwv_exprvars : vec VV (sac_numExprVars scbwv_sac)
+ ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types scbwv_sac Γ atypes)
+ ; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (vec2list
+ (vec_map (fun x => ((fst x),(snd x @@ weakL' lev))) scbwv_varstypes))