Uniform.lean

section disprob

parameters (Ω : Type) [fintype Ω]
parameters (uniform : Ω  → ℚ) 
parameters (Huniform : ∀ x : Ω, uniform x = 1 / (fintype.card Ω))


lemma prob_sum : match (fintype.exists_univ_list Ω) with 
     | (l, _) := list.sum (list.map l) = 1
     end :=
begin
   sorry 
end 

end disprob

invalid match/convoy expression, expected type is not knownLean