* Am 22.06.06 schrieb Matthew Walton: > When you say something like > > x : y = z > > in Epigram, what does Epigram understand = to be? What sort of equality > is this? It seems to be at some sort of value level, but seeing as how
It's reflexive equality. x acts as a witness that y equals z, such that for a type 0 = 1 there can be no such x. > it can work with function equality as well, it's obviously a little less > naïve than that. Yes, you're right and to have ∀ x => (f x) = (g x) -> f = g you need to undertake special efforts like Conor and Thorsten are doing with their 'Observational Typ Theory' http://www.cs.nott.ac.uk/~ctm/ott.pdf Best regards, Sebastian
