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

fix(library/init/lean/parser/declaration): axiom, constant, what's the difference

Browse source
This commit is contained in:
Sebastian Ullrich 2019-01-21 18:09:26 +01:00
parent abf60e3242
commit 814ceb43fe
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
library/init/lean/parser/declaration.lean
View file

@ -147,9 +147,10 @@ node! declaration [
name: ident_univ_params.parser, sig: opt_decl_sig.parser, val: decl_val.parser],
«instance»: node! «instance» ["instance", name: ident_univ_params.parser?, sig: decl_sig.parser, val: decl_val.parser],
«example»: node! «example» ["example", sig: decl_sig.parser, val: decl_val.parser],
«constant»: node! «constant» ["constant", name: ident_univ_params.parser, sig: decl_sig.parser],
«axiom»: node! «axiom» ["axiom", name: ident_univ_params.parser, sig: decl_sig.parser],
«constant»: node! «constant» [
kw: node_choice! constant_keyword {"constant", "axiom"},
name: ident_univ_params.parser,
sig: decl_sig.parser],
«inductive»: node! «inductive» [try [«class»: (symbol "class")?, "inductive"],
old_univ_params: old_univ_params.parser?,
name: ident_univ_params.parser,