Stream: new members

Topic: Simple Uniform Probability

Mukesh Tiwari (Dec 12 2019 at 11:40):

Hi Everyone, I am trying to model a simple proof, but I am getting "invalid match/convoy expression, expected type is not known" https://gist.github.com/mukeshtiwari/f5692ca8bacac1c2bcb44386194a0e2a

Reid Barton (Dec 12 2019 at 13:27):

I don't know how to account for that specific error message, but surely uniform should be mentioned somewhere in the statement.
But an easier way to write the statement is something like finset.univ.sum uniform = 1.

Last updated: May 06 2021 at 22:13 UTC