From eff43fab08e705cefb2cc3f26843cea4df6abc35 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 13 Oct 2018 07:59:45 -0700 Subject: [PATCH] chore(library/init/lean/expander): comment --- library/init/lean/expander.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean index 8694c4ded6..e69345b9bb 100644 --- a/library/init/lean/expander.lean +++ b/library/init/lean/expander.lean @@ -51,7 +51,7 @@ let prec := match sym with let prec_to_action := λ prec, {action.view . kind := action_kind.view.prec prec} in match k with | mixfix.kind.view.prefix _ := - -- `prefix tk:prec` ~> `notation tk:prec b:prec` + -- `prefix sym:prec` ~> `notation sym:prec b:prec` pure { rules := [{ symbol := sym,