[Agda] `case' vs `with'

[Nils Anders Danielsson]

On 2017-01-29 16:57, Sergei Meshveliani wrote:
> The below `case' version for `lemma' is not type-checked in Agda 2.5.2,
> while the `with' version is type-checked.
>
> I do not know of whether such `case' treating is intended in Agda,
> I report this for any occasion (because this difference looks strange).

The case_of_ function has a non-dependent type:

   case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
   case x of f = case x return _ of f

You could use case_return_of_ instead:

   case_return_of_ :
     ∀ {a b} {A : Set a}
     (x : A) (B : A → Set b) → ((x : A) → B x) → B x
   case x return B of f = f x

However, I suggest that you use with.

-- 
/NAD