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

chore(library/init/lean/ir/extract_cpp): add space

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-18 08:23:32 -07:00
parent ff725b8329
commit 2a13ea484e
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/ir/extract_cpp.lean
View file

@ -56,7 +56,7 @@ emit "(" *> a <* emit ")"
def comma (a b : extract_m unit) : extract_m unit :=
a *> emit ", " *> b
local infix `<+>`:65 := comma
local infix ` <+> `:65 := comma
def emit_var (x : var) : extract_m unit :=
emit $ name.mangle x "_x"