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

feat: use binop% to define arith operators

Browse source 
closes #382
This commit is contained in:
Leonardo de Moura 2021-04-30 19:40:45 -07:00
parent 9d934694e7
commit a2e8bc0780
2 changed files with 23 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Init/Notation.lean
View file

@ -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

8
tests/lean/run/382.lean Normal file
View file

@ -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)