diff --git a/library/algebra/field.lean b/library/algebra/field.lean index 5bb640df2..bfc1178f6 100644 --- a/library/algebra/field.lean +++ b/library/algebra/field.lean @@ -26,7 +26,7 @@ section division_ring include s definition divide (a b : A) : A := a * b⁻¹ - infix `/` := divide + infix [priority algebra.prio] `/` := divide -- only in this file local attribute divide [reducible] diff --git a/library/algebra/group.lean b/library/algebra/group.lean index 169339f98..360df42ab 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -7,7 +7,7 @@ Various multiplicative and additive structures. Partially modeled on Isabelle's -/ import logic.eq data.unit data.sigma data.prod -import algebra.function algebra.binary +import algebra.function algebra.binary algebra.priority open eq eq.ops -- note: ⁻¹ will be overloaded open binary @@ -36,12 +36,12 @@ structure has_inv [class] (A : Type) := structure has_neg [class] (A : Type) := (neg : A → A) -infixl `*` := has_mul.mul -infixl `+` := has_add.add -postfix `⁻¹` := has_inv.inv -prefix `-` := has_neg.neg -notation 1 := !has_one.one -notation 0 := !has_zero.zero +infixl [priority algebra.prio] `*` := has_mul.mul +infixl [priority algebra.prio] `+` := has_add.add +postfix [priority algebra.prio] `⁻¹` := has_inv.inv +prefix [priority algebra.prio] `-` := has_neg.neg +notation 1 := !has_one.one +notation 0 := !has_zero.zero /- semigroup -/ @@ -410,7 +410,7 @@ section add_group -- TODO: derive corresponding facts for div in a field definition sub [reducible] (a b : A) : A := a + -b - infix `-` := sub + infix [priority algebra.prio] `-` := sub theorem sub_eq_add_neg (a b : A) : a - b = a + -b := rfl diff --git a/library/algebra/group_power.lean b/library/algebra/group_power.lean index 586d27ae1..9143b6713 100644 --- a/library/algebra/group_power.lean +++ b/library/algebra/group_power.lean @@ -28,7 +28,7 @@ definition pow (a : A) : ℕ → A | 0 := 1 | (n+1) := pow n * a -infix `^` := pow +infix [priority algebra.prio] `^` := pow theorem pow_zero (a : A) : a^0 = 1 := rfl theorem pow_succ (a : A) (n : ℕ) : a^(succ n) = a^n * a := rfl @@ -92,7 +92,7 @@ theorem pow_inv_comm (a : A) : ∀m n, (a⁻¹)^m * a^n = a^n * (a⁻¹)^m end nat -open nat int algebra +open int definition ipow (a : A) : ℤ → A | (of_nat n) := a^n diff --git a/library/algebra/order.lean b/library/algebra/order.lean index e20650e31..e549024cc 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -5,7 +5,7 @@ Author: Jeremy Avigad Weak orders "≤", strict orders "<", and structures that include both. -/ -import logic.eq logic.connectives algebra.binary +import logic.eq logic.connectives algebra.binary algebra.priority open eq eq.ops namespace algebra @@ -20,16 +20,16 @@ structure has_le [class] (A : Type) := structure has_lt [class] (A : Type) := (lt : A → A → Prop) -infixl `<=` := has_le.le -infixl `≤` := has_le.le -infixl `<` := has_lt.lt +infixl [priority algebra.prio] `<=` := has_le.le +infixl [priority algebra.prio] `≤` := has_le.le +infixl [priority algebra.prio] `<` := has_lt.lt definition has_le.ge [reducible] {A : Type} [s : has_le A] (a b : A) := b ≤ a -notation a ≥ b := has_le.ge a b -notation a >= b := has_le.ge a b +notation [priority algebra.prio] a ≥ b := has_le.ge a b +notation [priority algebra.prio] a >= b := has_le.ge a b definition has_lt.gt [reducible] {A : Type} [s : has_lt A] (a b : A) := b < a -notation a > b := has_lt.gt a b +notation [priority algebra.prio] a > b := has_lt.gt a b /- weak orders -/ diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 56497c583..93d8b9af6 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -73,7 +73,7 @@ section comm_semiring include s definition dvd (a b : A) : Prop := ∃c, b = a * c - notation a ∣ b := dvd a b + notation [priority algebra.prio] a ∣ b := dvd a b theorem dvd.intro {a b c : A} (H : a * c = b) : a ∣ b := exists.intro _ H⁻¹ diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index aad571abe..12963345c 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -86,10 +86,12 @@ definition mul (a b : ℤ) : ℤ := /- notation -/ +protected definition prio : num := num.pred std.priority.default + notation `-[1+` n `]` := int.neg_succ_of_nat n -- for pretty-printing output -prefix - := int.neg -infix + := int.add -infix * := int.mul +prefix [priority int.prio] - := int.neg +infix [priority int.prio] + := int.add +infix [priority int.prio] * := int.mul /- some basic functions and properties -/ @@ -627,9 +629,9 @@ section migrate_algebra local attribute int.integral_domain [instance] definition sub (a b : ℤ) : ℤ := algebra.sub a b - infix - := int.sub + infix [priority int.prio] - := int.sub definition dvd (a b : ℤ) : Prop := algebra.dvd a b - notation a ∣ b := dvd a b + notation [priority int.prio] a ∣ b := dvd a b migrate from algebra with int replacing sub → sub, dvd → dvd diff --git a/library/data/int/div.lean b/library/data/int/div.lean index e4dc32492..67a21b9eb 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -23,11 +23,11 @@ sign b * | of_nat m := #nat m div (nat_abs b) | -[1+m] := -[1+ (#nat m div (nat_abs b))] end) -notation a div b := divide a b +notation [priority int.prio] a div b := divide a b definition modulo (a b : ℤ) : ℤ := a - a div b * b -notation a mod b := modulo a b -notation a `≡` b `[mod`:100 c `]`:0 := a mod c = b mod c +notation [priority int.prio] a mod b := modulo a b +notation [priority int.prio] a `≡` b `[mod`:100 c `]`:0 := a mod c = b mod c /- div -/ diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 636d02d02..0e11aec92 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -18,10 +18,10 @@ private definition nonneg (a : ℤ) : Prop := int.cases_on a (take n, true) (tak definition le (a b : ℤ) : Prop := nonneg (sub b a) definition lt (a b : ℤ) : Prop := le (add a 1) b -infix - := int.sub -infix <= := int.le -infix ≤ := int.le -infix < := int.lt +infix [priority int.prio] - := int.sub +infix [priority int.prio] <= := int.le +infix [priority int.prio] ≤ := int.le +infix [priority int.prio] < := int.lt local attribute nonneg [reducible] private definition decidable_nonneg [instance] (a : ℤ) : decidable (nonneg a) := int.cases_on a _ _ diff --git a/library/data/int/power.lean b/library/data/int/power.lean index 930c4749a..dcfd2a837 100644 --- a/library/data/int/power.lean +++ b/library/data/int/power.lean @@ -17,7 +17,7 @@ section migrate_algebra local attribute int.decidable_linear_ordered_comm_ring [instance] definition pow (a : ℤ) (n : ℕ) : ℤ := algebra.pow a n - infix ^ := pow + infix [priority int.prio] ^ := pow migrate from algebra with int replacing dvd → dvd, has_le.ge → ge, has_lt.gt → gt, pow → pow diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index e8f4992c5..1c97bc994 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -371,14 +371,16 @@ definition denom (a : ℚ) : ℤ := prerat.denom (reduce a) theorem denom_pos (a : ℚ): denom a > 0 := prerat.denom_pos (reduce a) -infix + := rat.add -infix * := rat.mul -prefix - := rat.neg +protected definition prio := num.pred int.prio + +infix [priority rat.prio] + := rat.add +infix [priority rat.prio] * := rat.mul +prefix [priority rat.prio] - := rat.neg definition sub [reducible] (a b : rat) : rat := a + (-b) -postfix ⁻¹ := rat.inv -infix - := rat.sub +postfix [priority rat.prio] ⁻¹ := rat.inv +infix [priority rat.prio] - := rat.sub /- properties -/ diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean index ac219acbe..93e98d17b 100644 --- a/library/data/rat/order.lean +++ b/library/data/rat/order.lean @@ -146,12 +146,12 @@ definition le (a b : ℚ) : Prop := nonneg (b - a) definition gt [reducible] (a b : ℚ) := lt b a definition ge [reducible] (a b : ℚ) := le b a -infix < := rat.lt -infix <= := rat.le -infix ≤ := rat.le -infix >= := rat.ge -infix ≥ := rat.ge -infix > := rat.gt +infix [priority rat.prio] < := rat.lt +infix [priority rat.prio] <= := rat.le +infix [priority rat.prio] ≤ := rat.le +infix [priority rat.prio] >= := rat.ge +infix [priority rat.prio] ≥ := rat.ge +infix [priority rat.prio] > := rat.gt theorem of_int_lt_of_int (a b : ℤ) : of_int a < of_int b ↔ (#int a < b) := iff.symm (calc diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean index 1e65bf4c9..91273bfec 100644 --- a/library/data/real/basic.lean +++ b/library/data/real/basic.lean @@ -1003,18 +1003,19 @@ definition add (x y : ℝ) : ℝ := (quot.lift_on₂ x y (λ a b, quot.mk (a + b)) (take a b c d : reg_seq, take Hab : requiv a c, take Hcd : requiv b d, quot.sound (radd_well_defined Hab Hcd))) -infix `+` := add +protected definition prio := num.pred rat.prio +infix [priority real.prio] `+` := add definition mul (x y : ℝ) : ℝ := (quot.lift_on₂ x y (λ a b, quot.mk (a * b)) (take a b c d : reg_seq, take Hab : requiv a c, take Hcd : requiv b d, quot.sound (rmul_well_defined Hab Hcd))) -infix `*` := mul +infix [priority real.prio] `*` := mul definition neg (x : ℝ) : ℝ := (quot.lift_on x (λ a, quot.mk (-a)) (take a b : reg_seq, take Hab : requiv a b, quot.sound (rneg_well_defined Hab))) -prefix `-` := neg +prefix [priority real.prio] `-` := neg definition zero : ℝ := quot.mk r_zero --notation 0 := zero diff --git a/library/data/real/division.lean b/library/data/real/division.lean index 04a27435f..08ade03ee 100644 --- a/library/data/real/division.lean +++ b/library/data/real/division.lean @@ -610,7 +610,7 @@ open [classes] s definition inv (x : ℝ) : ℝ := quot.lift_on x (λ a, quot.mk (s.r_inv a)) (λ a b H, quot.sound (s.r_inv_well_defined H)) -postfix `⁻¹` := inv +postfix [priority real.prio] `⁻¹` := inv theorem le_total (x y : ℝ) : x ≤ y ∨ y ≤ x := quot.induction_on₂ x y (λ s t, s.r_le_total s t) diff --git a/library/data/real/order.lean b/library/data/real/order.lean index 4e621eb61..6a2099a78 100644 --- a/library/data/real/order.lean +++ b/library/data/real/order.lean @@ -1018,18 +1018,18 @@ open [classes] s namespace real definition lt (x y : ℝ) := quot.lift_on₂ x y (λ a b, s.r_lt a b) s.r_lt_well_defined -infix `<` := lt +infix [priority real.prio] `<` := lt definition le (x y : ℝ) := quot.lift_on₂ x y (λ a b, s.r_le a b) s.r_le_well_defined -infix `≤` := le -infix `<=` := le +infix [priority real.prio] `≤` := le +infix [priority real.prio] `<=` := le definition gt [reducible] (a b : ℝ) := lt b a definition ge [reducible] (a b : ℝ) := le b a -infix >= := real.ge -infix ≥ := real.ge -infix > := real.gt +infix [priority real.prio] >= := real.ge +infix [priority real.prio] ≥ := real.ge +infix [priority real.prio] > := real.gt definition sep (x y : ℝ) := quot.lift_on₂ x y (λ a b, s.r_sep a b) s.r_sep_well_defined infix `≢` : 50 := sep @@ -1114,9 +1114,9 @@ section migrate_algebra local attribute real.ordered_ring [instance] definition sub (a b : ℝ) : ℝ := algebra.sub a b - infix - := real.sub + infix [priority real.prio] - := real.sub definition dvd (a b : ℝ) : Prop := algebra.dvd a b - notation a ∣ b := real.dvd a b + notation [priority real.prio] a ∣ b := real.dvd a b migrate from algebra with real replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, dvd → dvd, divide → divide diff --git a/tests/lean/notation_priority.lean b/tests/lean/notation_priority.lean new file mode 100644 index 000000000..dd3d098ab --- /dev/null +++ b/tests/lean/notation_priority.lean @@ -0,0 +1,26 @@ +import data.real + +open real int nat + +variables a b : nat +variables i j : int + +set_option pp.all true +check a + b +check i + j + +example : a + b = nat.add a b := +rfl +example : i + j = int.add i j := +rfl + +open nat real int + +example : a + b = nat.add a b := +rfl +example : i + j = int.add i j := +rfl + +set_option pp.all true +check a + b +check i + j diff --git a/tests/lean/notation_priority.lean.expected.out b/tests/lean/notation_priority.lean.expected.out new file mode 100644 index 000000000..049aace77 --- /dev/null +++ b/tests/lean/notation_priority.lean.expected.out @@ -0,0 +1,4 @@ +nat.add a b : nat +int.add i j : int +nat.add a b : nat +int.add i j : int diff --git a/tests/lua/parse_table.lua b/tests/lua/parse_table.lua deleted file mode 100644 index 676cccd97..000000000 --- a/tests/lua/parse_table.lua +++ /dev/null @@ -1,119 +0,0 @@ -function display_parse_table(t) - t:for_each(function(ts, es) - if not t:is_nud() then - io.write("_ ") - end - for i = 1, #ts do - io.write("'" .. tostring(ts[i][1]) .. "'") - local a = ts[i][2] - local k = a:kind() - if k == notation_action_kind.Skip then - elseif k == notation_action_kind.Binder then - io.write(" binder") - elseif k == notation_action_kind.Binders then - io.write(" binders") - elseif k == notation_action_kind.Ext then - io.write(" external") - elseif k == notation_action_kind.ScopedExpr then - io.write(" [_@" .. tostring(a:rbp()) .. ":" .. tostring(a:rec()) .. "]") - elseif k == notation_action_kind.Expr then - if a:rbp() == 0 then - io.write(" _") - else - io.write(" _@" .. tostring(a:rbp())) - end - elseif k == notation_action_kind.Exprs then - io.write(" [" .. tostring(a:rbp()) .. ", " .. tostring(a:rec()) .. ", " .. tostring(a:ini()) .. ", " .. tostring(a:is_fold_right()) .. "]") - end - io.write(" ") - end - print(":= ") - while (not es:is_nil()) do - print(" " .. tostring(es:head())) - es = es:tail() - end - end) -end - -function parse_table_size(t) - local r = 0 - t:for_each(function(ts, es) r = r + #es end) - return r -end - -local p = parse_table() -assert(is_parse_table(p)) -local ite = Const("ite") -local ite2 = Const("ite2") -local If = Const("if") -p = p:add({"if", "then", "else"}, ite(Var(0), Var(1), Var(2))) -p = p:add({"if", "then", "else"}, ite2(Var(0), Var(1), Var(2))) -p = p:add({"if", "then"}, If(Var(0), Var(1))) -display_parse_table(p) -assert(parse_table_size(p) == 3) -p = p:add({"if", "then", "else"}, ite2(Var(0), Var(1), Var(2)), false) -print("======") -display_parse_table(p) -assert(parse_table_size(p) == 2) -local f = Const("f") -p = p:add({{"with", Skip}, "value"}, f(Var(0))) -local Exists = Const("Exists") -local ExistUnique = Const("ExistUnique") -p = p:add({{"exists", Binders}, {",", scoped_expr_notation_action(Exists(Var(0)))}}, Var(0)) -p = p:add({{"exist!", Binder}, {",", scoped_expr_notation_action(ExistUnique(Var(0)))}}, Var(0)) -print("======") -display_parse_table(p) -check_error(function() p = p:add({{"with", Skip}, "value"}, f(Var(1))) end) -check_error(function() - p = p:add({{",", scoped_expr_notation_action(Exists(Var(0)))}}, Var(0)) -end) -local nat_add = Const({"nat", "add"}) -local int_add = Const({"int", "add"}) -check_error(function() p = p:add({{"+", 10}}, nat_add(Var(0), Var(1))) end) -p = p:add({"if", "then", "else"}, ite(Var(0), Var(1), Var(2))) -local a, p2 = p:find("if") -assert(is_notation_action(a)) -assert(a:kind() == notation_action_kind.Expr) -assert(a:rbp() == 0) -print("======") -display_parse_table(p2) -assert(parse_table_size(p2) == 3) -local _, p2 = p2:find("then") -local _, p2 = p2:find("else") -print("======") -assert(parse_table_size(p2) == 2) -display_parse_table(p2) -local es = p2:is_accepting() -assert(es) -assert(#es == 2) - -local p = parse_table(false) -- Create led table -assert(not p:is_nud()) -p = p:add({{"+", 10}}, nat_add(Var(0), Var(1))) -p = p:add({{"+", 10}}, int_add(Var(0), Var(1))) -print("======") -display_parse_table(p) - -local nat_mul = Const({"nat", "mul"}) -local int_mul = Const({"int", "mul"}) -local p2 = parse_table(false) -- Create led table -p2 = p2:add({{"*", 20}}, nat_mul(Var(0), Var(1))) -p2 = p2:add({{"*", 20}}, int_mul(Var(0), Var(1))) -print("======") -display_parse_table(p2) - -p = p:merge(p2) -print("======") -display_parse_table(p) -assert(parse_table_size(p) == 4) - -local p3 = parse_table() -check_error(function() p:merge(p3) end) - -local a = scoped_expr_notation_action(Var(0), 10) -assert(a:use_lambda_abstraction()) -local a = scoped_expr_notation_action(Var(0), 10, false) -assert(not a:use_lambda_abstraction()) -local a = scoped_expr_notation_action(Var(0), 10, true) -assert(a:use_lambda_abstraction()) -assert(a:rbp() == 10)