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

fix: workaround for old frontend

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-15 15:49:45 -08:00
parent 3ee6aec466
commit f4db2f5971
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/Lean/Compiler/ExternAttr.lean
View file

@ -57,9 +57,9 @@ private partial def syntaxToExternEntries (a : Array Syntax) (i : Nat) (entries
private def syntaxToExternAttrData (s : Syntax) : ExceptT String Id ExternAttrData :=
match s with
| Syntax.missing => Except.ok { entries := [ ExternEntry.adhoc `all ] }
| Syntax.node _ args =>
if args.size == 0 then Except.error "unexpected kind of argument"
if args.size == 0 then
Except.ok { entries := [ ExternEntry.adhoc `all ] }
else
let (arity, i) : Option Nat × Nat := match args[0].isNatLit? with
| some arity => (some arity, 1)