Compare commits

...

1 Commits

Author SHA1 Message Date
Leonardo de Moura
46e697355b chore: missing double backticks 2024-03-03 18:45:16 -08:00
2 changed files with 3 additions and 3 deletions

View File

@@ -19,7 +19,7 @@ structure CaseArraySizesSubgoal where
def getArrayArgType (a : Expr) : MetaM Expr := do
let aType inferType a
let aType whnfD aType
unless aType.isAppOfArity `Array 1 do
unless aType.isAppOfArity ``Array 1 do
throwError "array expected{indentExpr a}"
pure aType.appArg!

View File

@@ -87,7 +87,7 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do
let c' := c ++ ctx.varName
let cinfo getConstInfo c
let resultTy forallTelescope cinfo.type fun _ b => pure b
if resultTy.isConstOf `Lean.Parser.TrailingParser || resultTy.isConstOf `Lean.Parser.Parser then do
if resultTy.isConstOf ``Lean.Parser.TrailingParser || resultTy.isConstOf ``Lean.Parser.Parser then do
-- synthesize a new `[combinatorAttr c]`
let some value pure cinfo.value?
| throwError "don't know how to generate {ctx.varName} for non-definition '{e}'"
@@ -146,7 +146,7 @@ unsafe def registerParserCompiler {α} (ctx : Context α) : IO Unit := do
Parser.registerParserAttributeHook {
postAdd := fun catName constName builtin => do
let info getConstInfo constName
if info.type.isConstOf `Lean.ParserDescr || info.type.isConstOf `Lean.TrailingParserDescr then
if info.type.isConstOf ``Lean.ParserDescr || info.type.isConstOf ``Lean.TrailingParserDescr then
let d evalConstCheck ParserDescr `Lean.ParserDescr constName <|>
evalConstCheck TrailingParserDescr `Lean.TrailingParserDescr constName
compileEmbeddedParsers ctx d (builtin := builtin) |>.run'