Could not parse with pattern

[ice1000]

Simple, minimum code to reproduce the error:

parseF : List ℂ → List Fmt
parseF [] = []
parseF (x ∷ xs) with xs | x ≟ '%'
...         | '%' ∷ xss | (yes y) = {!!}

The code above uses these declarations:

open import Data.List using (List; _∷_; [])
open import Data.Char renaming (Char to ℂ; show to showℂ)

data Fmt : Set where
  fmt : ℂ → Fmt
  lit : ℂ → Fmt

If I change (yes y) to y, the parser works. But I need to pattern match on x ≟ '%', how can I do that?

[ice1000]

And of course use C-c C-c to do a case split on y causes a parse error:

parseF : List ℂ → List Fmt
parseF [] = []
parseF (x ∷ xs) with xs | x ≟ '%'
parseF (x ∷ xs) | '%' ∷ xss | .Relation.Nullary.Dec.yes p = ?
parseF (x ∷ xs) | '%' ∷ xss | .Relation.Nullary.Dec.no ¬p = ?

[gallais]

You need to open import Relation.Nullary so that yes is in scope. Otherwise Agda
does not know about yes and thinks you are trying to declare a pattern of the form
(function argument) which is illegal.

[ice1000]

Ok thanks

[ice1000]

@gallais And BTW why Agda complains about the termination of this function?

parseF : List ℂ → List Fmt
parseF [] = []
parseF (x ∷ xs) with xs | x ≟ '%'
...         | '%' ∷ xss | yes _ = lit '%' ∷ parseF xss
...         |  c  ∷ xss | yes _ = fmt c ∷ parseF xss
...         | [] | yes _ = lit '%' ∷ []
...         | _  | no  _ = lit x ∷ parseF xs

[ice1000]

While the normal form checks:

parseF : List ℂ → List Fmt
parseF [] = []
parseF ('%' ∷ '%' ∷ cs) = lit '%' ∷ parseF cs
parseF ('%' ∷  c  ∷ cs) = fmt c ∷ parseF cs
parseF ( c  ∷  cs) = lit c ∷ parseF cs

[ice1000]

Moved discussion to #3173