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

feat: add helper command

Browse source
This commit is contained in:
Leonardo de Moura 2021-05-13 22:10:35 -07:00
parent f850820029
commit 71cd067e94
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Parser/Command.lean
View file

@ -99,6 +99,11 @@ def openDecl := openHiding <|> openRenaming <|> openOnly <|> openSimple
@[builtinCommandParser] def «in» := trailing_parser " in " >> commandParser
/-
This is an auxiliary command for generation constructor injectivity theorems for inductive types defined at `Prelude.lean`.
It is meant for bootstrapping purposes only. -/
@[builtinCommandParser] def genInjectiveTheorems := leading_parser "gen_injective_theorems% " >> ident
@[runBuiltinParserAttributeHooks] abbrev declModifiersF := declModifiers false
@[runBuiltinParserAttributeHooks] abbrev declModifiersT := declModifiers true