Idris: è possibile riscrivere tutte le funzioni utilizzando "with" per utilizzare "case" anziché "with"? Se no, potresti dare un controesempio?

Question

In Idris, è possibile riscrivere tutte le funzioni utilizzando "with" per utilizzare "caso" anziché "con"?

In caso contrario, potresti fornire un esempio di contatore?

Answer 1

Non possibile. Quando si esegue lo schema di corrispondenza con with, i tipi nel contesto vengono aggiornati con le informazioni estratte dal costruttore corrispondente. case non causa questo aggiornamento.

A titolo di esempio, le seguenti opere con with ma non con 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