Search code examples
idris

Pattern-match (destructure) in equality proof

data T = A String | B String

p : ((A s) = (A s')) -> (s = s')

If I have (A s) = (A s'), how do I obtain s = s'?

P.S. I'm new to Idris. Feel free to edit my question for code style or to add pertinent keywords.

Solution

  • Pattern match on Refl:

    data T = A String | B String

p : ((A s) = (A s')) -> (s = s')
p Refl = Refl