Idris: Is it possible to rewrite all functions using "c" to use "case" instead of "c"? If not, can you give a counter example?

Question

In Idris, is it possible to rewrite all functions with using "use" case "instead of" with "?

If not, can you give a counter example?

Answer 1

Impossible. When you map a template to with , the types in the context are updated with information extracted from the associated constructor. case does not cause such an update.

As an example, the following works with , but not case :

 import Data.So -- here (n == 10) in the goal type is rewritten to True or False -- after the match maybeTen : (n : Nat) -> Maybe (So (n == 10)) maybeTen n with (n == 10) maybeTen n | False = Nothing maybeTen n | True = Just Oh -- Here the context knows nothing about the result of (n == 10) -- after the "case" match, so we can't fill in the rhs maybeTen' : (n : Nat) -> Maybe (So (n == 10)) maybeTen' n = case (n == 10) of True => ?a False => ?b