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

chore: remove arity

Browse source 
@Kha I improved the arity calculation for `extern`s.
This commit is contained in:
Leonardo de Moura 2020-08-31 16:38:39 -07:00
parent 5da3d9bf70
commit 821b1c2b6c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/PrettyPrinter/Formatter.lean
View file

@ -185,7 +185,7 @@ p1 <|> p2
-- Note that there is a mutual recursion
-- `categoryParser -> mkAntiquot -> termParser -> categoryParser`, so we need to introduce an indirection somewhere
-- anyway.
@[extern 8 "lean_mk_antiquot_formatter"]
@[extern "lean_mk_antiquot_formatter"]
constant mkAntiquot.formatter' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Formatter :=
arbitrary _