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

revert: panic! changes

Browse source 
@Kha I am reverting this change for now.
I understand that the "default-value" approach is bad for debugging,
and it does not produce good error messages, but at least the frontend
will not "panic" when users add a bad macro.

After we switch to the new frontend, we can have a monadic `getArg`
and `getArgs` in the Elab and Macro monads which produces an
"unexpected syntax" error message. I say we wait for the new frontend
because we will be able to write `(<- s.getArg)` inside of
expressions.
This commit is contained in:
Leonardo de Moura 2020-08-19 09:57:58 -07:00
parent 1840b4b1ff
commit 57ed29e814
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/LeanInit.lean
View file

@ -223,12 +223,12 @@ def isOfKind : Syntax → SyntaxNodeKind → Bool
def getArg (stx : Syntax) (i : Nat) : Syntax :=
match stx with
| Syntax.node _ args => args.get! i
| _ => panic! "Syntax.getArg: not a node"
| _ => Syntax.missing -- panic! "Syntax.getArg: not a node"
def getArgs (stx : Syntax) : Array Syntax :=
match stx with
| Syntax.node _ args => args
| _ => panic! "Syntax.getArgs: not a node"
| _ => #[] -- panic! "Syntax.getArgs: not a node"
/-- Retrieve the left-most leaf's info in the Syntax tree. -/
partial def getHeadInfo : Syntax → Option SourceInfo