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

feat: use binrel_no_prop% to define == notation

Browse source 
fixes #764
This commit is contained in:
Leonardo de Moura 2021-11-09 07:46:10 -08:00
parent b70820929f
commit 743810b77a
2 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Notation.lean
View file

@ -113,7 +113,7 @@ macro_rules | `($x > $y) => `(binrel% GT.gt $x $y)
macro_rules | `($x >= $y) => `(binrel% GE.ge $x $y)
macro_rules | `($x ≥ $y) => `(binrel% GE.ge $x $y)
macro_rules | `($x = $y) => `(binrel% Eq $x $y)
macro_rules | `($x == $y) => `(binrel% BEq.beq $x $y)
macro_rules | `($x == $y) => `(binrel_no_prop% BEq.beq $x $y)
infixr:35 " /\\ " => And
infixr:35 " ∧ " => And

6
tests/lean/run/764.lean Normal file
View file

@ -0,0 +1,6 @@
#eval (5 > 2) == true
#eval (2 > 5) == true
variable (b : Bool)
#check (5 > 2) == b