Open
Description
In the following code block:
Id : Set
Id = String
convert : ℕ -> Id -> Expr -> DeBruijn
convert ind id (var x) with id ≟ x
... | p = {!p!}when I split on p I get:
convert : ℕ -> Id -> Expr -> DeBruijn
convert ind id (var x) with id ≟ x
convert ind id (var x) | Relation.Nullary.Dec.yes p = ?
convert ind id (var x) | Relation.Nullary.Dec.no ¬p = ?along with the error message:
Could not parse the left-hand side
convert ind id (var x) | Relation.Nullary.Dec.yes p
Operators used in the grammar:
None
when scope checking the left-hand side
convert ind id (var x) | Relation.Nullary.Dec.yes p in the
definition of convert
This is a result of Relation.Nullary not being in scope. I think this error message for a parse error generated by a case split is not ideal and it would be better if it were able to say that the module is not in scope.