add case0 to syntax since that is possible sometimes

This commit is contained in:
rhiannon morris 2023-04-02 15:22:39 +02:00
parent 3f3079c48d
commit 38dbd275a1
3 changed files with 3 additions and 3 deletions

View file

@ -165,7 +165,7 @@ lamIntro = symbolsC [(Lam, "λ"), (DLam, "δ")]
private covering
caseIntro : Grammar True Qty
caseIntro = symbols [(One, "case1"), (Any, "caseω")]
caseIntro = symbols [(Zero, "case0"), (One, "case1"), (Any, "caseω")]
<|> resC "case" *>
(qty <* resC "." <|>
fatalError {c = True} "missing quantity on 'case'")