-
- 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))
+ Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)}{sac:@StrongAltCon tc} :=
+ { scbwv_exprvars : vec VV (sac_numExprVars sac)
+ ; scbwv_exprvars_distinct : distinct (vec2list scbwv_exprvars)
+ ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types sac Γ atypes)
+ ; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes)