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

fix(library/init/lean/compiler/ir/emitcpp): typo

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-21 16:21:21 -07:00
parent 8003ccec13
commit 40b890f220
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/lean/compiler/ir/emitcpp.lean
View file

@ -425,7 +425,7 @@ match decl with
match mkExternCall extData `cpp (toStringArgs ys) with
| some c := emit c *> emitLn ";"
| none := throw "failed to emit extern application"
| _ := do emitCppName f, when (ys.size > 0) (do emit "(", emitArgs ys, emitLn ")"), emitLn ";"
| _ := do emitCppName f, when (ys.size > 0) (do emit "(", emitArgs ys, emit ")"), emitLn ";"
def emitPartialApp (z : VarId) (f : FunId) (ys : Array Arg) : M Unit :=
do