Inconsistency between syntax and kind names
#1090
Comments
leodemoura
added a commit
that referenced
this issue
Apr 1, 2022
TODO: remove staging workarounds see #1090
leodemoura
added a commit
that referenced
this issue
Apr 1, 2022
Josh-Tilles
added a commit
to Josh-Tilles/macro-supplement
that referenced
this issue
Apr 20, 2022
See: <leanprover/lean4#1090> Addresses errors: ```sh-session $ lean Bigop.lean bigop 0 [0, 2, 4] fun i => (i, Add.add, i != 2, i) : Nat bigop 0 (index_iota 10 20) fun i => (i, Add.add, i != 5, i + 1) : Nat bigop 0 (index_iota 10 20) fun i => (i, Add.add, true, i + 1) : Nat bigop 1 [0, 2, 4] fun i => (i, Mul.mul, i != 2, i) : Nat bigop 1 (index_iota 10 20) fun i => (i, Mul.mul, i != 5, i + 1) : Nat bigop 1 (index_iota 10 20) fun i => (i, Mul.mul, true, i + 1) : Nat bigop 0 Enumerable.elems fun i => (i, Add.add, true, i + 1) : Fin 10 bigop 0 Enumerable.elems fun i => (i, Add.add, i != 2, i + 1) : Fin 10 bigop 0 Enumerable.elems fun i => (i, Add.add, myPred i, i + i) : Fin 10 bigop 1 Enumerable.elems fun i => (i, Mul.mul, true, i + 1) : Fin 10 bigop 1 Enumerable.elems fun i => (i, Mul.mul, i != 2, i + 1) : Fin 10 bigop 1 Enumerable.elems fun i => (i, Mul.mul, myPred i, i + i) : Fin 10 bigop 0 (index_iota 10 20) fun i => (i, Add.add, true, i + 1) : Nat Bigop.lean:119:12: error: expected '&', '(', '[', 'atom', 'binary', 'cat', 'ident', 'macroArg', 'nonReserved', 'paren', 'sepBy', 'sepBy(', 'sepBy1', 'sepBy1(', 'str', 'stx', 'unary', identifier or string literal Bigop.lean:121:0: error: elaboration function for 'Bigop.commandDef_bigop___' has not been implemented Bigop.lean:122:14: error: expected ')' $ lean Expander.lean Expander.lean:127:6: error: expected '#check', '#check_failure', '#eval', '#exit', '#print', '#reduce', '#resolve_name', '#synth', '/-!', '`(tactic|', 'abbrev', 'attribute', 'axiom', 'builtin_initialize', 'check', 'check_failure', 'class', 'classInductive', 'classTk', 'command', 'constant', 'declaration', 'declare_syntax_cat', 'def', 'deriving', 'elab', 'elab_rules', 'end', 'eval', 'example', 'exit', 'export', 'genInjectiveTheorems', 'gen_injective_theorems%', 'inductive', 'infix', 'infixl', 'infixr', 'init_quot', 'initialize', 'instance', 'macro', 'macro_rules', 'mixfix', 'moduleDoc', 'mutual', 'namespace', 'noncomputable', 'noncomputableSection', 'notation', 'open', 'postfix', 'prefix', 'print', 'printAxioms', 'quot', 'reduce', 'resolve_name', 'section', 'set_option', 'structure', 'structureTk', 'syntax', 'syntaxAbbrev', 'syntaxCat', 'synth', 'term', 'theorem', 'unif_hint', 'universe', 'variable' or identifier Expander.lean:134:10: error: expected identifier Expander.lean:136:10: error: expected identifier Expander.lean:138:13: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal Expander.lean:138:89: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal Expander.lean:140:20: error: expected '`(tactic|' Expander.lean:143:20: error: expected '`(tactic|' Expander.lean:198:6: error: expected '#check', '#check_failure', '#eval', '#exit', '#print', '#reduce', '#resolve_name', '#synth', '/-!', '`(tactic|', 'abbrev', 'attribute', 'axiom', 'builtin_initialize', 'check', 'check_failure', 'class', 'classInductive', 'classTk', 'command', 'constant', 'declaration', 'declare_syntax_cat', 'def', 'deriving', 'elab', 'elab_rules', 'end', 'eval', 'example', 'exit', 'export', 'genInjectiveTheorems', 'gen_injective_theorems%', 'inductive', 'infix', 'infixl', 'infixr', 'init_quot', 'initialize', 'instance', 'macro', 'macro_rules', 'mixfix', 'moduleDoc', 'mutual', 'namespace', 'noncomputable', 'noncomputableSection', 'notation', 'open', 'postfix', 'prefix', 'print', 'printAxioms', 'quot', 'reduce', 'resolve_name', 'section', 'set_option', 'structure', 'structureTk', 'syntax', 'syntaxAbbrev', 'syntaxCat', 'synth', 'term', 'theorem', 'unif_hint', 'universe', 'variable' or identifier Expander.lean:201:10: error: expected identifier Expander.lean:202:13: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal Expander.lean:203:20: error: expected '`(tactic|' Expander.lean:301:0: error: cannot evaluate code because 'Lean.Expander.expand' uses 'sorry' and/or contains errors Expander.lean:308:0: error: cannot evaluate code because 'Lean.Expander.expand' uses 'sorry' and/or contains errors ```
Josh-Tilles
added a commit
to Josh-Tilles/macro-supplement
that referenced
this issue
Apr 20, 2022
See: <leanprover/lean4#1090> Addresses errors: ```sh-session $ lean Bigop.lean bigop 0 [0, 2, 4] fun i => (i, Add.add, i != 2, i) : Nat bigop 0 (index_iota 10 20) fun i => (i, Add.add, i != 5, i + 1) : Nat bigop 0 (index_iota 10 20) fun i => (i, Add.add, true, i + 1) : Nat bigop 1 [0, 2, 4] fun i => (i, Mul.mul, i != 2, i) : Nat bigop 1 (index_iota 10 20) fun i => (i, Mul.mul, i != 5, i + 1) : Nat bigop 1 (index_iota 10 20) fun i => (i, Mul.mul, true, i + 1) : Nat bigop 0 Enumerable.elems fun i => (i, Add.add, true, i + 1) : Fin 10 bigop 0 Enumerable.elems fun i => (i, Add.add, i != 2, i + 1) : Fin 10 bigop 0 Enumerable.elems fun i => (i, Add.add, myPred i, i + i) : Fin 10 bigop 1 Enumerable.elems fun i => (i, Mul.mul, true, i + 1) : Fin 10 bigop 1 Enumerable.elems fun i => (i, Mul.mul, i != 2, i + 1) : Fin 10 bigop 1 Enumerable.elems fun i => (i, Mul.mul, myPred i, i + i) : Fin 10 bigop 0 (index_iota 10 20) fun i => (i, Add.add, true, i + 1) : Nat Bigop.lean:119:12: error: expected '&', '(', '[', 'atom', 'binary', 'cat', 'ident', 'macroArg', 'nonReserved', 'paren', 'sepBy', 'sepBy(', 'sepBy1', 'sepBy1(', 'str', 'stx', 'unary', identifier or string literal Bigop.lean:121:0: error: elaboration function for 'Bigop.commandDef_bigop___' has not been implemented Bigop.lean:122:14: error: expected ')' $ lean Expander.lean Expander.lean:127:6: error: expected '#check', '#check_failure', '#eval', '#exit', '#print', '#reduce', '#resolve_name', '#synth', '/-!', '`(tactic|', 'abbrev', 'attribute', 'axiom', 'builtin_initialize', 'check', 'check_failure', 'class', 'classInductive', 'classTk', 'command', 'constant', 'declaration', 'declare_syntax_cat', 'def', 'deriving', 'elab', 'elab_rules', 'end', 'eval', 'example', 'exit', 'export', 'genInjectiveTheorems', 'gen_injective_theorems%', 'inductive', 'infix', 'infixl', 'infixr', 'init_quot', 'initialize', 'instance', 'macro', 'macro_rules', 'mixfix', 'moduleDoc', 'mutual', 'namespace', 'noncomputable', 'noncomputableSection', 'notation', 'open', 'postfix', 'prefix', 'print', 'printAxioms', 'quot', 'reduce', 'resolve_name', 'section', 'set_option', 'structure', 'structureTk', 'syntax', 'syntaxAbbrev', 'syntaxCat', 'synth', 'term', 'theorem', 'unif_hint', 'universe', 'variable' or identifier Expander.lean:134:10: error: expected identifier Expander.lean:136:10: error: expected identifier Expander.lean:138:13: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal Expander.lean:138:89: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal Expander.lean:140:20: error: expected '`(tactic|' Expander.lean:143:20: error: expected '`(tactic|' Expander.lean:198:6: error: expected '#check', '#check_failure', '#eval', '#exit', '#print', '#reduce', '#resolve_name', '#synth', '/-!', '`(tactic|', 'abbrev', 'attribute', 'axiom', 'builtin_initialize', 'check', 'check_failure', 'class', 'classInductive', 'classTk', 'command', 'constant', 'declaration', 'declare_syntax_cat', 'def', 'deriving', 'elab', 'elab_rules', 'end', 'eval', 'example', 'exit', 'export', 'genInjectiveTheorems', 'gen_injective_theorems%', 'inductive', 'infix', 'infixl', 'infixr', 'init_quot', 'initialize', 'instance', 'macro', 'macro_rules', 'mixfix', 'moduleDoc', 'mutual', 'namespace', 'noncomputable', 'noncomputableSection', 'notation', 'open', 'postfix', 'prefix', 'print', 'printAxioms', 'quot', 'reduce', 'resolve_name', 'section', 'set_option', 'structure', 'structureTk', 'syntax', 'syntaxAbbrev', 'syntaxCat', 'synth', 'term', 'theorem', 'unif_hint', 'universe', 'variable' or identifier Expander.lean:201:10: error: expected identifier Expander.lean:202:13: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal Expander.lean:203:20: error: expected '`(tactic|' Expander.lean:301:0: error: cannot evaluate code because 'Lean.Expander.expand' uses 'sorry' and/or contains errors Expander.lean:308:0: error: cannot evaluate code because 'Lean.Expander.expand' uses 'sorry' and/or contains errors ```
Josh-Tilles
added a commit
to Josh-Tilles/macro-supplement
that referenced
this issue
Apr 20, 2022
See: <leanprover/lean4#1090> Addresses errors: ```sh-session $ lean Bigop.lean bigop 0 [0, 2, 4] fun i => (i, Add.add, i != 2, i) : Nat bigop 0 (index_iota 10 20) fun i => (i, Add.add, i != 5, i + 1) : Nat bigop 0 (index_iota 10 20) fun i => (i, Add.add, true, i + 1) : Nat bigop 1 [0, 2, 4] fun i => (i, Mul.mul, i != 2, i) : Nat bigop 1 (index_iota 10 20) fun i => (i, Mul.mul, i != 5, i + 1) : Nat bigop 1 (index_iota 10 20) fun i => (i, Mul.mul, true, i + 1) : Nat bigop 0 Enumerable.elems fun i => (i, Add.add, true, i + 1) : Fin 10 bigop 0 Enumerable.elems fun i => (i, Add.add, i != 2, i + 1) : Fin 10 bigop 0 Enumerable.elems fun i => (i, Add.add, myPred i, i + i) : Fin 10 bigop 1 Enumerable.elems fun i => (i, Mul.mul, true, i + 1) : Fin 10 bigop 1 Enumerable.elems fun i => (i, Mul.mul, i != 2, i + 1) : Fin 10 bigop 1 Enumerable.elems fun i => (i, Mul.mul, myPred i, i + i) : Fin 10 bigop 0 (index_iota 10 20) fun i => (i, Add.add, true, i + 1) : Nat Bigop.lean:119:12: error: expected '&', '(', '[', 'atom', 'binary', 'cat', 'ident', 'macroArg', 'nonReserved', 'paren', 'sepBy', 'sepBy(', 'sepBy1', 'sepBy1(', 'str', 'stx', 'unary', identifier or string literal Bigop.lean:121:0: error: elaboration function for 'Bigop.commandDef_bigop___' has not been implemented Bigop.lean:122:14: error: expected ')' $ lean Expander.lean Expander.lean:127:6: error: expected '#check', '#check_failure', '#eval', '#exit', '#print', '#reduce', '#resolve_name', '#synth', '/-!', '`(tactic|', 'abbrev', 'attribute', 'axiom', 'builtin_initialize', 'check', 'check_failure', 'class', 'classInductive', 'classTk', 'command', 'constant', 'declaration', 'declare_syntax_cat', 'def', 'deriving', 'elab', 'elab_rules', 'end', 'eval', 'example', 'exit', 'export', 'genInjectiveTheorems', 'gen_injective_theorems%', 'inductive', 'infix', 'infixl', 'infixr', 'init_quot', 'initialize', 'instance', 'macro', 'macro_rules', 'mixfix', 'moduleDoc', 'mutual', 'namespace', 'noncomputable', 'noncomputableSection', 'notation', 'open', 'postfix', 'prefix', 'print', 'printAxioms', 'quot', 'reduce', 'resolve_name', 'section', 'set_option', 'structure', 'structureTk', 'syntax', 'syntaxAbbrev', 'syntaxCat', 'synth', 'term', 'theorem', 'unif_hint', 'universe', 'variable' or identifier Expander.lean:134:10: error: expected identifier Expander.lean:136:10: error: expected identifier Expander.lean:138:13: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal Expander.lean:138:89: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal Expander.lean:140:20: error: expected '`(tactic|' Expander.lean:143:20: error: expected '`(tactic|' Expander.lean:198:6: error: expected '#check', '#check_failure', '#eval', '#exit', '#print', '#reduce', '#resolve_name', '#synth', '/-!', '`(tactic|', 'abbrev', 'attribute', 'axiom', 'builtin_initialize', 'check', 'check_failure', 'class', 'classInductive', 'classTk', 'command', 'constant', 'declaration', 'declare_syntax_cat', 'def', 'deriving', 'elab', 'elab_rules', 'end', 'eval', 'example', 'exit', 'export', 'genInjectiveTheorems', 'gen_injective_theorems%', 'inductive', 'infix', 'infixl', 'infixr', 'init_quot', 'initialize', 'instance', 'macro', 'macro_rules', 'mixfix', 'moduleDoc', 'mutual', 'namespace', 'noncomputable', 'noncomputableSection', 'notation', 'open', 'postfix', 'prefix', 'print', 'printAxioms', 'quot', 'reduce', 'resolve_name', 'section', 'set_option', 'structure', 'structureTk', 'syntax', 'syntaxAbbrev', 'syntaxCat', 'synth', 'term', 'theorem', 'unif_hint', 'universe', 'variable' or identifier Expander.lean:201:10: error: expected identifier Expander.lean:202:13: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal Expander.lean:203:20: error: expected '`(tactic|' Expander.lean:300:0: error: cannot evaluate code because 'Lean.Expander.expand' uses 'sorry' and/or contains errors Expander.lean:307:0: error: cannot evaluate code because 'Lean.Expander.expand' uses 'sorry' and/or contains errors ```
Kha
pushed a commit
to Kha/macro-supplement
that referenced
this issue
Apr 21, 2022
See: <leanprover/lean4#1090> Addresses errors: ```sh-session $ lean Bigop.lean bigop 0 [0, 2, 4] fun i => (i, Add.add, i != 2, i) : Nat bigop 0 (index_iota 10 20) fun i => (i, Add.add, i != 5, i + 1) : Nat bigop 0 (index_iota 10 20) fun i => (i, Add.add, true, i + 1) : Nat bigop 1 [0, 2, 4] fun i => (i, Mul.mul, i != 2, i) : Nat bigop 1 (index_iota 10 20) fun i => (i, Mul.mul, i != 5, i + 1) : Nat bigop 1 (index_iota 10 20) fun i => (i, Mul.mul, true, i + 1) : Nat bigop 0 Enumerable.elems fun i => (i, Add.add, true, i + 1) : Fin 10 bigop 0 Enumerable.elems fun i => (i, Add.add, i != 2, i + 1) : Fin 10 bigop 0 Enumerable.elems fun i => (i, Add.add, myPred i, i + i) : Fin 10 bigop 1 Enumerable.elems fun i => (i, Mul.mul, true, i + 1) : Fin 10 bigop 1 Enumerable.elems fun i => (i, Mul.mul, i != 2, i + 1) : Fin 10 bigop 1 Enumerable.elems fun i => (i, Mul.mul, myPred i, i + i) : Fin 10 bigop 0 (index_iota 10 20) fun i => (i, Add.add, true, i + 1) : Nat Bigop.lean:119:12: error: expected '&', '(', '[', 'atom', 'binary', 'cat', 'ident', 'macroArg', 'nonReserved', 'paren', 'sepBy', 'sepBy(', 'sepBy1', 'sepBy1(', 'str', 'stx', 'unary', identifier or string literal Bigop.lean:121:0: error: elaboration function for 'Bigop.commandDef_bigop___' has not been implemented Bigop.lean:122:14: error: expected ')' $ lean Expander.lean Expander.lean:127:6: error: expected '#check', '#check_failure', '#eval', '#exit', '#print', '#reduce', '#resolve_name', '#synth', '/-!', '`(tactic|', 'abbrev', 'attribute', 'axiom', 'builtin_initialize', 'check', 'check_failure', 'class', 'classInductive', 'classTk', 'command', 'constant', 'declaration', 'declare_syntax_cat', 'def', 'deriving', 'elab', 'elab_rules', 'end', 'eval', 'example', 'exit', 'export', 'genInjectiveTheorems', 'gen_injective_theorems%', 'inductive', 'infix', 'infixl', 'infixr', 'init_quot', 'initialize', 'instance', 'macro', 'macro_rules', 'mixfix', 'moduleDoc', 'mutual', 'namespace', 'noncomputable', 'noncomputableSection', 'notation', 'open', 'postfix', 'prefix', 'print', 'printAxioms', 'quot', 'reduce', 'resolve_name', 'section', 'set_option', 'structure', 'structureTk', 'syntax', 'syntaxAbbrev', 'syntaxCat', 'synth', 'term', 'theorem', 'unif_hint', 'universe', 'variable' or identifier Expander.lean:134:10: error: expected identifier Expander.lean:136:10: error: expected identifier Expander.lean:138:13: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal Expander.lean:138:89: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal Expander.lean:140:20: error: expected '`(tactic|' Expander.lean:143:20: error: expected '`(tactic|' Expander.lean:198:6: error: expected '#check', '#check_failure', '#eval', '#exit', '#print', '#reduce', '#resolve_name', '#synth', '/-!', '`(tactic|', 'abbrev', 'attribute', 'axiom', 'builtin_initialize', 'check', 'check_failure', 'class', 'classInductive', 'classTk', 'command', 'constant', 'declaration', 'declare_syntax_cat', 'def', 'deriving', 'elab', 'elab_rules', 'end', 'eval', 'example', 'exit', 'export', 'genInjectiveTheorems', 'gen_injective_theorems%', 'inductive', 'infix', 'infixl', 'infixr', 'init_quot', 'initialize', 'instance', 'macro', 'macro_rules', 'mixfix', 'moduleDoc', 'mutual', 'namespace', 'noncomputable', 'noncomputableSection', 'notation', 'open', 'postfix', 'prefix', 'print', 'printAxioms', 'quot', 'reduce', 'resolve_name', 'section', 'set_option', 'structure', 'structureTk', 'syntax', 'syntaxAbbrev', 'syntaxCat', 'synth', 'term', 'theorem', 'unif_hint', 'universe', 'variable' or identifier Expander.lean:201:10: error: expected identifier Expander.lean:202:13: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal Expander.lean:203:20: error: expected '`(tactic|' Expander.lean:300:0: error: cannot evaluate code because 'Lean.Expander.expand' uses 'sorry' and/or contains errors Expander.lean:307:0: error: cannot evaluate code because 'Lean.Expander.expand' uses 'sorry' and/or contains errors ```
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The
numsyntaxproduces thenumLitkind (and in particular antiquotation kind),strproducesstrLitetc.. This is quite confusing when writing a syntax quotation for a syntax. We should rename the syntax or the kind. TheLitdoes add semantic information, but I have a slight preference for the shorter names as they should still be sufficiently unambiguous.The text was updated successfully, but these errors were encountered: