CODEWITHSUNDEEP
idris
Jo Liss
Jo Liss

Reputation: 32945

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.

Upvotes: 1

Views: 68

Answers (1)

michaelmesser
michaelmesser

Reputation: 3726

Pattern match on Refl:

data T = A String | B String

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

Upvotes: 2

Related Questions