From a2e8bc0780c349c5c6f599b10d7d443537fe6972 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 30 Apr 2021 19:40:45 -0700 Subject: [PATCH] feat: use `binop%` to define arith operators closes #382 --- src/Init/Notation.lean | 15 +++++++++++++++ tests/lean/run/382.lean | 8 ++++++++ 2 files changed, 23 insertions(+) create mode 100644 tests/lean/run/382.lean diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index bec2fc570f..7e018bddb5 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -76,6 +76,21 @@ infixl:75 " >>> " => HShiftRight.hShiftRight infixr:80 " ^ " => HPow.hPow prefix:100 "-" => Neg.neg prefix:100 "~~~" => Complement.complement +/- + Remark: the infix commands above ensure a delaborator is generated for each relations. + We redefine the macros below to be able to use the auxiliary `binop%` elaboration helper for binary operators. + It addresses issue #382. -/ +macro_rules | `($x ||| $y) => `(binop% HOr.hOr $x $y) +macro_rules | `($x ^^^ $y) => `(binop% HXor.hXor $x $y) +macro_rules | `($x &&& $y) => `(binop% HAnd.hAnd $x $y) +macro_rules | `($x + $y) => `(binop% HAdd.hAdd $x $y) +macro_rules | `($x - $y) => `(binop% HSub.hSub $x $y) +macro_rules | `($x * $y) => `(binop% HMul.hMul $x $y) +macro_rules | `($x / $y) => `(binop% HDiv.hDiv $x $y) +macro_rules | `($x % $y) => `(binop% HMod.hMod $x $y) +macro_rules | `($x <<< $y) => `(binop% HShiftLeft.hShiftLeft $x $y) +macro_rules | `($x >>> $y) => `(binop% HShiftRight.hShiftRight $x $y) +macro_rules | `($x ^ $y) => `(binop% HPow.hPow $x $y) -- declare ASCII alternatives first so that the latter Unicode unexpander wins infix:50 " <= " => LE.le diff --git a/tests/lean/run/382.lean b/tests/lean/run/382.lean new file mode 100644 index 0000000000..c0923f8daa --- /dev/null +++ b/tests/lean/run/382.lean @@ -0,0 +1,8 @@ +variable (n k : Nat) +set_option pp.all true +#check n+k +#check (n + k : Int) +#check (n + 1 : Int) +#check (2 + n : Int) +#check (1 + 2 : Int) +#check (1 + 2 * 3 : UInt32)