CODEWITHSUNDEEP
idris
MantasG
MantasG

Reputation: 117

Equality proofs and pattern matching in total functions

I know this is a bit contrived example, but I was wondering how do I make the following function total: 

total foo : (x : Int) -> {auto prf : x = 10} -> Int
foo 10 = 10

At the moment type checker complains:

Main.foo is not total as there are missing cases

Edit:

Adding impossible branch to HTNWs answer I got it to typecheck this way:

total foo : (x : Int) -> {auto prf : x = 10} -> Int
foo 10 {prf = Refl} = 10
foo x {prf = Refl} impossible

Upvotes: 1

Views: 82

Answers (1)

HTNW
HTNW

Reputation: 29193

You have to pattern match on the equality, too

total foo : (x : Int) -> {auto prf : x = 10} -> Int
foo 10 {prf=Refl} = 10

Upvotes: 2

Related Questions