- Record StrongCaseBranchWithVVs {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} :=
- { scbwv_scb : @StrongCaseBranch n tc Γ atypes
- ; scbwv_exprvars : vec VV (saci_numExprVars scbwv_scb)
- ; scbwv_varstypes := vec2list (vec_zip scbwv_exprvars (scb_types scbwv_scb))
+ Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:vec (HaskType Γ) 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))