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

doc: typos and indentation

Browse source
This commit is contained in:
Mario Carneiro 2022-08-12 09:02:07 -04:00 • committed by Leonardo de Moura
parent d1beded289
commit 311d376bde
1 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/Lean/Elab/Util.lean
View file

@ -107,7 +107,7 @@ unsafe def mkElabAttribute (γ) (attrDeclName attrBuiltinName attrName : Name) (
valueTypeName := typeName
evalKey := fun _ stx => do
let kind ← syntaxNodeKindOfAttrParam parserNamespace stx
/- Recall that a `SyntaxNodeKind` is often the name of the paser, but this is not always true, and we much check it. -/
/- Recall that a `SyntaxNodeKind` is often the name of the parser, but this is not always true, and we must check it. -/
if (← getEnv).contains kind && (← getInfoState).enabled then
pushInfoLeaf <| Info.ofTermInfo {
elaborator := .anonymous
@ -119,10 +119,10 @@ unsafe def mkElabAttribute (γ) (attrDeclName attrBuiltinName attrName : Name) (
return kind
onAdded := fun builtin declName => do
if builtin then
if let some doc ← findDocString? (← getEnv) declName then
declareBuiltin (declName ++ `docString) (mkAppN (mkConst ``addBuiltinDocString) #[toExpr declName, toExpr doc])
if let some declRanges ← findDeclarationRanges? declName then
declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges])
if let some doc ← findDocString? (← getEnv) declName then
declareBuiltin (declName ++ `docString) (mkAppN (mkConst ``addBuiltinDocString) #[toExpr declName, toExpr doc])
if let some declRanges ← findDeclarationRanges? declName then
declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges])
} attrDeclName
unsafe def mkMacroAttributeUnsafe : IO (KeyedDeclsAttribute Macro) :=
@ -199,11 +199,11 @@ partial def mkUnusedBaseName (baseName : Name) : MacroM Name := do
let currNamespace ← Macro.getCurrNamespace
if ← Macro.hasDecl (currNamespace ++ baseName) then
let rec loop (idx : Nat) := do
let name := baseName.appendIndexAfter idx
if ← Macro.hasDecl (currNamespace ++ name) then
loop (idx+1)
else
return name
let name := baseName.appendIndexAfter idx
if ← Macro.hasDecl (currNamespace ++ name) then
loop (idx+1)
else
return name
loop 1
else
return baseName