max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: missing double backticks (#3587)

Browse source
This commit is contained in:
Leonardo de Moura 2024-03-03 19:02:35 -08:00 • committed by GitHub
parent bba4ef3728
commit e6d6855a85
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/Match/CaseArraySizes.lean
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!

4
src/Lean/ParserCompiler.lean
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'