From baf4c01de8a662d57b2d110ef51900197f4a4400 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 17 Sep 2014 14:39:05 -0700 Subject: [PATCH] feat(frontends/lean): definitions are opaque by default --- library/algebra/binary.lean | 4 +-- library/algebra/category.lean | 10 +++--- library/algebra/function.lean | 18 +++++------ library/algebra/relation.lean | 22 +++++++------- library/data/bool.lean | 6 ++-- library/data/int/basic.lean | 30 ++++++------------ library/data/int/order.lean | 1 + library/data/list/basic.lean | 2 +- library/data/nat/basic.lean | 13 +++----- library/data/nat/div.lean | 1 + library/data/nat/order.lean | 4 +-- library/data/nat/sub.lean | 1 + library/data/num.lean | 26 ++++++++-------- library/data/prod.lean | 6 ++-- library/data/quotient/basic.lean | 7 ++--- library/data/quotient/util.lean | 2 +- library/data/sigma.lean | 4 +-- library/data/sum.lean | 4 +-- library/data/vector.lean | 2 +- library/hott/equiv.lean | 2 +- library/hott/path.lean | 13 +++----- library/hott/trunc.lean | 6 ++-- library/logic/axioms/hilbert.lean | 2 +- library/logic/core/connectives.lean | 2 +- library/logic/core/decidable.lean | 4 +-- library/logic/core/eq.lean | 4 +-- library/logic/core/instances.lean | 10 +++--- library/logic/core/prop.lean | 8 ++--- library/logic/core/quantifiers.lean | 2 +- library/tools/fake_simplifier.lean | 2 +- library/tools/helper_tactics.lean | 2 +- library/tools/tactic.lean | 44 +++++++++++++-------------- src/emacs/lean-company.el | 2 +- src/emacs/lean-syntax.el | 4 +-- src/frontends/lean/decl_cmds.cpp | 18 +++++------ src/frontends/lean/token_table.cpp | 4 +-- src/library/tactic/expr_to_tactic.cpp | 2 +- src/library/typed_expr.cpp | 8 ++--- tests/lean/bug1.lean | 4 +-- tests/lean/calc1.lean | 2 +- tests/lean/run/algebra1.lean | 30 +++++++++--------- tests/lean/run/basic.lean | 4 +-- tests/lean/run/cat.lean | 6 ++-- tests/lean/run/class5.lean | 2 +- tests/lean/run/class_bug1.lean | 4 +-- tests/lean/run/class_bug2.lean | 4 +-- tests/lean/run/class_coe.lean | 2 +- tests/lean/run/cody1.lean | 2 +- tests/lean/run/cody2.lean | 2 +- tests/lean/run/congr_imp_bug.lean | 4 +-- tests/lean/run/e1.lean | 2 +- tests/lean/run/e14.lean | 4 +-- tests/lean/run/e2.lean | 2 +- tests/lean/run/e3.lean | 3 +- tests/lean/run/e4.lean | 3 +- tests/lean/run/e5.lean | 8 ++--- tests/lean/run/elab_bug1.lean | 2 +- tests/lean/run/group.lean | 2 +- tests/lean/run/group2.lean | 4 +-- tests/lean/run/have1.lean | 4 +-- tests/lean/run/have2.lean | 2 +- tests/lean/run/have3.lean | 4 +-- tests/lean/run/have4.lean | 4 +-- tests/lean/run/have6.lean | 2 +- tests/lean/run/impbug1.lean | 4 +-- tests/lean/run/impbug2.lean | 4 +-- tests/lean/run/impbug3.lean | 4 +-- tests/lean/run/impbug4.lean | 4 +-- tests/lean/run/ind5.lean | 2 +- tests/lean/run/indimp.lean | 2 +- tests/lean/run/induniv.lean | 2 +- tests/lean/run/n3.lean | 2 +- tests/lean/run/n4.lean | 2 +- tests/lean/run/nat_bug.lean | 2 +- tests/lean/run/nat_bug2.lean | 4 +-- tests/lean/run/nat_bug3.lean | 4 +-- tests/lean/run/nat_coe.lean | 4 +-- tests/lean/run/over_subst.lean | 2 +- tests/lean/run/simple.lean | 4 +-- tests/lean/run/sum_bug.lean | 4 +-- tests/lean/run/t9.lean | 2 +- tests/lean/run/tactic23.lean | 8 ++--- tests/lean/run/trans.lean | 2 +- tests/lean/run/uuu.lean | 10 +++--- tests/lean/run/whnfinst.lean | 2 +- tests/lean/slow/list_elab2.lean | 2 +- tests/lean/slow/nat_bug1.lean | 4 +-- tests/lean/slow/nat_bug2.lean | 12 ++++---- tests/lean/slow/nat_wo_hints.lean | 4 +-- tests/lean/slow/path_groupoids.lean | 15 +++++---- tests/lean/t4.lean | 2 +- 91 files changed, 251 insertions(+), 276 deletions(-) diff --git a/library/algebra/binary.lean b/library/algebra/binary.lean index 2803ad305..be3d8f38c 100644 --- a/library/algebra/binary.lean +++ b/library/algebra/binary.lean @@ -9,8 +9,8 @@ namespace binary parameter {A : Type} parameter f : A → A → A infixl `*`:75 := f - abbreviation commutative := ∀{a b}, a*b = b*a - abbreviation associative := ∀{a b c}, (a*b)*c = a*(b*c) + definition commutative := ∀{a b}, a*b = b*a + definition associative := ∀{a b c}, (a*b)*c = a*(b*c) end context diff --git a/library/algebra/category.lean b/library/algebra/category.lean index 32647b143..00e95e314 100644 --- a/library/algebra/category.lean +++ b/library/algebra/category.lean @@ -24,13 +24,13 @@ namespace category section parameters {ob : Type} {Cat : category ob} {A B C D : ob} - abbreviation mor : ob → ob → Type := rec (λ mor compose id assoc idr idl, mor) Cat - abbreviation compose : Π {A B C : ob}, mor B C → mor A B → mor A C := + definition mor : ob → ob → Type := rec (λ mor compose id assoc idr idl, mor) Cat + definition compose : Π {A B C : ob}, mor B C → mor A B → mor A C := rec (λ mor compose id assoc idr idl, compose) Cat - abbreviation id : Π {A : ob}, mor A A := + definition id : Π {A : ob}, mor A A := rec (λ mor compose id assoc idr idl, id) Cat - abbreviation ID (A : ob) : mor A A := @id A + definition ID (A : ob) : mor A A := @id A infixr `∘` := compose @@ -190,7 +190,7 @@ namespace category section parameter {ob : Type} - abbreviation opposite (C : category ob) : category ob := + definition opposite (C : category ob) : category ob := category.mk (λa b, mor b a) (λ a b c f g, g ∘ f) (λ a, id) (λ a b c d f g h, symm assoc) (λ a b f, id_left) (λ a b f, id_right) precedence `∘op` : 60 diff --git a/library/algebra/function.lean b/library/algebra/function.lean index 100badc32..8c5f7c7bc 100644 --- a/library/algebra/function.lean +++ b/library/algebra/function.lean @@ -6,33 +6,33 @@ namespace function section parameters {A : Type} {B : Type} {C : Type} {D : Type} {E : Type} - abbreviation compose (f : B → C) (g : A → B) : A → C := + definition compose (f : B → C) (g : A → B) : A → C := λx, f (g x) - abbreviation id (a : A) : A := + definition id (a : A) : A := a - abbreviation on_fun (f : B → B → C) (g : A → B) : A → A → C := + definition on_fun (f : B → B → C) (g : A → B) : A → A → C := λx y, f (g x) (g y) - abbreviation combine (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E := + definition combine (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E := λx y, op (f x y) (g x y) end -abbreviation const {A : Type} (B : Type) (a : A) : B → A := +definition const {A : Type} (B : Type) (a : A) : B → A := λx, a -abbreviation dcompose {A : Type} {B : A → Type} {C : Π {x : A}, B x → Type} (f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) := +definition dcompose {A : Type} {B : A → Type} {C : Π {x : A}, B x → Type} (f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) := λx, f (g x) -abbreviation flip {A : Type} {B : Type} {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y := +definition flip {A : Type} {B : Type} {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y := λy x, f x y -abbreviation app {A : Type} {B : A → Type} (f : Πx, B x) (x : A) : B x := +definition app {A : Type} {B : A → Type} (f : Πx, B x) (x : A) : B x := f x -- Yet another trick to anotate an expression with a type -abbreviation is_typeof (A : Type) (a : A) : A := +definition is_typeof (A : Type) (a : A) : A := a precedence `∘`:60 diff --git a/library/algebra/relation.lean b/library/algebra/relation.lean index 10916f8cf..81d6717d0 100644 --- a/library/algebra/relation.lean +++ b/library/algebra/relation.lean @@ -13,9 +13,9 @@ import logic.core.prop namespace relation -abbreviation reflexive {T : Type} (R : T → T → Type) : Type := ∀x, R x x -abbreviation symmetric {T : Type} (R : T → T → Type) : Type := ∀⦃x y⦄, R x y → R y x -abbreviation transitive {T : Type} (R : T → T → Type) : Type := ∀⦃x y z⦄, R x y → R y z → R x z +definition reflexive {T : Type} (R : T → T → Type) : Type := ∀x, R x x +definition symmetric {T : Type} (R : T → T → Type) : Type := ∀⦃x y⦄, R x y → R y x +definition transitive {T : Type} (R : T → T → Type) : Type := ∀⦃x y z⦄, R x y → R y z → R x z inductive is_reflexive {T : Type} (R : T → T → Type) : Prop := @@ -23,10 +23,10 @@ mk : reflexive R → is_reflexive R namespace is_reflexive - abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : is_reflexive R) : reflexive R := + definition app ⦃T : Type⦄ {R : T → T → Type} (C : is_reflexive R) : reflexive R := is_reflexive.rec (λu, u) C - abbreviation infer ⦃T : Type⦄ (R : T → T → Type) {C : is_reflexive R} : reflexive R := + definition infer ⦃T : Type⦄ (R : T → T → Type) {C : is_reflexive R} : reflexive R := is_reflexive.rec (λu, u) C end is_reflexive @@ -37,10 +37,10 @@ mk : symmetric R → is_symmetric R namespace is_symmetric - abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : is_symmetric R) : symmetric R := + definition app ⦃T : Type⦄ {R : T → T → Type} (C : is_symmetric R) : symmetric R := is_symmetric.rec (λu, u) C - abbreviation infer ⦃T : Type⦄ (R : T → T → Type) {C : is_symmetric R} : symmetric R := + definition infer ⦃T : Type⦄ (R : T → T → Type) {C : is_symmetric R} : symmetric R := is_symmetric.rec (λu, u) C end is_symmetric @@ -51,10 +51,10 @@ mk : transitive R → is_transitive R namespace is_transitive - abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : is_transitive R) : transitive R := + definition app ⦃T : Type⦄ {R : T → T → Type} (C : is_transitive R) : transitive R := is_transitive.rec (λu, u) C - abbreviation infer ⦃T : Type⦄ (R : T → T → Type) {C : is_transitive R} : transitive R := + definition infer ⦃T : Type⦄ (R : T → T → Type) {C : is_transitive R} : transitive R := is_transitive.rec (λu, u) C end is_transitive @@ -102,7 +102,7 @@ mk : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 namespace congruence - abbreviation app {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop} + definition app {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop} {f : T1 → T2} (C : congruence R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) := rec (λu, u) C x y @@ -110,7 +110,7 @@ namespace congruence (f : T1 → T2) {C : congruence R1 R2 f} ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) := rec (λu, u) C x y - abbreviation app2 {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop} + definition app2 {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop} {T3 : Type} {R3 : T3 → T3 → Prop} {f : T1 → T2 → T3} (C : congruence2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄ : R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) := diff --git a/library/data/bool.lean b/library/data/bool.lean index c09303b80..cb591d982 100644 --- a/library/data/bool.lean +++ b/library/data/bool.lean @@ -10,13 +10,13 @@ inductive bool : Type := ff : bool, tt : bool namespace bool - abbreviation rec_on [protected] {C : bool → Type} (b : bool) (H₁ : C ff) (H₂ : C tt) : C b := + definition rec_on [protected] {C : bool → Type} (b : bool) (H₁ : C ff) (H₂ : C tt) : C b := rec H₁ H₂ b - abbreviation cases_on [protected] {p : bool → Prop} (b : bool) (H₁ : p ff) (H₂ : p tt) : p b := + definition cases_on [protected] {p : bool → Prop} (b : bool) (H₁ : p ff) (H₂ : p tt) : p b := rec H₁ H₂ b - abbreviation cond {A : Type} (b : bool) (t e : A) := + definition cond {A : Type} (b : bool) (t e : A) := rec_on b e t theorem dichotomy (b : bool) : b = ff ∨ b = tt := diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 1ba4088fb..ca0ba10a5 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -18,7 +18,7 @@ open eq_ops namespace int -- ## The defining equivalence relation on ℕ × ℕ -abbreviation rel (a b : ℕ × ℕ) : Prop := pr1 a + pr2 b = pr2 a + pr1 b +definition rel (a b : ℕ × ℕ) : Prop := pr1 a + pr2 b = pr2 a + pr1 b theorem rel_comp (n m k l : ℕ) : (rel (pair n m) (pair k l)) ↔ (n + l = m + k) := have H : (pr1 (pair n m) + pr2 (pair k l) = pr2 (pair n m) + pr1 (pair k l)) ↔ (n + l = m + k), @@ -105,7 +105,7 @@ theorem proj_flip (a : ℕ × ℕ) : proj (flip a) = flip (proj a) := have special : ∀a, pr2 a ≤ pr1 a → proj (flip a) = flip (proj a), from take a, assume H : pr2 a ≤ pr1 a, - have H2 : pr1 (flip a) ≤ pr2 (flip a), from P_flip H, + have H2 : pr1 (flip a) ≤ pr2 (flip a), from P_flip a H, have H3 : pr1 (proj (flip a)) = pr1 (flip (proj a)), from calc pr1 (proj (flip a)) = 0 : proj_le_pr1 H2 @@ -122,7 +122,7 @@ have special : ∀a, pr2 a ≤ pr1 a → proj (flip a) = flip (proj a), from or.elim le_total (assume H : pr2 a ≤ pr1 a, special a H) (assume H : pr1 a ≤ pr2 a, - have H2 : pr2 (flip a) ≤ pr1 (flip a), from P_flip H, + have H2 : pr2 (flip a) ≤ pr1 (flip a), from P_flip a H, calc proj (flip a) = flip (flip (proj (flip a))) : (flip_flip (proj (flip a)))⁻¹ ... = flip (proj (flip (flip a))) : {(special (flip a) H2)⁻¹} @@ -143,6 +143,7 @@ or.elim le_total ... = pr2 a + 0 : add_zero_right⁻¹ ... = pr2 a + pr1 (proj a) : {(proj_le_pr1 H)⁻¹}) +opaque add sub le theorem proj_congr {a b : ℕ × ℕ} (H : rel a b) : proj a = proj b := have special : ∀a b, pr2 a ≤ pr1 a → rel a b → proj a = proj b, from take a b, @@ -166,7 +167,7 @@ have special : ∀a b, pr2 a ≤ pr1 a → rel a b → proj a = proj b, from or.elim le_total (assume H2 : pr2 a ≤ pr1 a, special a b H2 H) (assume H2 : pr1 a ≤ pr2 a, - have H3 : pr2 (flip a) ≤ pr1 (flip a), from P_flip H2, + have H3 : pr2 (flip a) ≤ pr1 (flip a), from P_flip a H2, have H4 : proj (flip a) = proj (flip b), from special (flip a) (flip b) H3 (rel_flip H), have H5 : flip (proj a) = flip (proj b), from proj_flip a ▸ proj_flip b ▸ H4, show proj a = proj b, from flip_inj H5) @@ -184,11 +185,11 @@ representative_map_idempotent_equiv proj_rel @proj_congr a -- ## Definition of ℤ and basic theorems and definitions -definition int [protected] := image proj +definition int [opaque] [protected] := image proj notation `ℤ` := int -definition psub : ℕ × ℕ → ℤ := fun_image proj -definition rep : ℤ → ℕ × ℕ := subtype.elt_of +definition psub [opaque] : ℕ × ℕ → ℤ := fun_image proj +definition rep [opaque] : ℤ → ℕ × ℕ := subtype.elt_of theorem quotient : is_quotient rel psub rep := representative_map_to_quotient_equiv rel_equiv proj_rel @proj_congr @@ -763,16 +764,5 @@ not_intro theorem mul_ne_zero_right {a b : ℤ} (H : a * b ≠ 0) : b ≠ 0 := mul_ne_zero_left (mul_comm a b ▸ H) --- set_opaque rel true --- set_opaque rep true --- set_opaque of_nat true --- set_opaque to_nat true --- set_opaque neg true --- set_opaque add true --- set_opaque mul true --- set_opaque le true --- set_opaque lt true --- set_opaque sign true ---transparent: sub ge gt -end int -- namespace int -abbreviation int := int.int +end int +definition int := int.int diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 314bb4892..ba75d96bb 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -133,6 +133,7 @@ discriminate -- ### interaction with neg and sub +opaque le neg theorem le_neg {a b : ℤ} (H : a ≤ b) : -b ≤ -a := obtain (n : ℕ) (Hn : a + n = b), from le_elim H, have H2 : b - n = a, from add_imp_sub_right Hn, diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 0de7819f6..f9c2f13e8 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -37,7 +37,7 @@ theorem cases_on [protected] {P : list T → Prop} (l : list T) (Hnil : P nil) (Hcons : ∀ (x : T) (l : list T), P (x::l)) : P l := induction_on l Hnil (take x l IH, Hcons x l) -abbreviation rec_on [protected] {A : Type} {C : list A → Type} (l : list A) +definition rec_on [protected] {A : Type} {C : list A → Type} (l : list A) (H1 : C nil) (H2 : Π (h : A) (t : list A), C t → C (h::t)) : C l := rec H1 H2 l diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index dbdc9c2a3..f1cc14ce6 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -43,13 +43,13 @@ inhabited.mk zero -- Coercion from num -- ----------------- -abbreviation plus (x y : ℕ) : ℕ := +definition add (x y : ℕ) : ℕ := nat.rec x (λ n r, succ r) y +infixl `+` := add -definition to_nat [coercion] [inline] (n : num) : ℕ := +definition to_nat [coercion] (n : num) : ℕ := num.rec zero - (λ n, pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n - + (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n -- Successor and predecessor -- ------------------------- @@ -150,11 +150,6 @@ general m -- Addition -- -------- - -definition add (x y : ℕ) : ℕ := plus x y - -infixl `+` := add - theorem add_zero_right {n : ℕ} : n + 0 = n theorem add_succ_right {n m : ℕ} : n + succ m = succ (n + m) diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 78eb3a7b9..87486e292 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -305,6 +305,7 @@ case_zero_pos n (by simp) -- add_rewrite mod_mul_self_right +opaque add mul theorem mod_mul_self_left {m n : ℕ} : (m * n) mod m = 0 := mul_comm ▸ mod_mul_self_right diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 3acd482d7..72bb493b7 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -258,11 +258,11 @@ general n definition lt (n m : ℕ) := succ n ≤ m infix `<` := lt -abbreviation ge (n m : ℕ) := m ≤ n +definition ge (n m : ℕ) := m ≤ n infix `>=` := ge infix `≥` := ge -abbreviation gt (n m : ℕ) := m < n +definition gt (n m : ℕ) := m < n infix `>` := gt theorem lt_def (n m : ℕ) : (n < m) = (succ n ≤ m) := rfl diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index fdd733a51..d4905d9d1 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -67,6 +67,7 @@ induction_on k ... = (n + l) - (m + l) : sub_succ_succ ... = n - m : IH) +opaque add mul le theorem sub_add_add_left {k n m : ℕ} : (k + n) - (k + m) = n - m := add_comm ▸ add_comm ▸ sub_add_add_right diff --git a/library/data/num.lean b/library/data/num.lean index c3b4e7c6a..ab22b99d8 100644 --- a/library/data/num.lean +++ b/library/data/num.lean @@ -22,20 +22,20 @@ namespace pos_num (H₁ : P one) (H₂ : ∀ (n : pos_num), P n → P (bit1 n)) (H₃ : ∀ (n : pos_num), P n → P (bit0 n)) : P a := rec H₁ H₂ H₃ a - abbreviation rec_on [protected] {P : pos_num → Type} (a : pos_num) + definition rec_on [protected] {P : pos_num → Type} (a : pos_num) (H₁ : P one) (H₂ : ∀ (n : pos_num), P n → P (bit1 n)) (H₃ : ∀ (n : pos_num), P n → P (bit0 n)) : P a := rec H₁ H₂ H₃ a - abbreviation succ (a : pos_num) : pos_num := + definition succ (a : pos_num) : pos_num := rec_on a (bit0 one) (λn r, bit0 r) (λn r, bit1 n) - abbreviation is_one (a : pos_num) : bool := + definition is_one (a : pos_num) : bool := rec_on a tt (λn r, ff) (λn r, ff) - abbreviation pred (a : pos_num) : pos_num := + definition pred (a : pos_num) : pos_num := rec_on a one (λn r, bit0 n) (λn r, cond (is_one n) one (bit1 r)) - abbreviation size (a : pos_num) : pos_num := + definition size (a : pos_num) : pos_num := rec_on a one (λn r, succ r) (λn r, succ r) theorem succ_not_is_one {a : pos_num} : is_one (succ a) = ff := @@ -51,7 +51,7 @@ namespace pos_num ... = bit1 n : {iH}) (take (n : pos_num) (iH : pred (succ n) = n), rfl) - abbreviation add (a b : pos_num) : pos_num := + definition add (a b : pos_num) : pos_num := rec_on a succ (λn f b, rec_on b @@ -93,7 +93,7 @@ namespace pos_num theorem add_bit1_bit1 {a b : pos_num} : (bit1 a) + (bit1 b) = succ (bit1 (a + b)) := rfl - abbreviation mul (a b : pos_num) : pos_num := + definition mul (a b : pos_num) : pos_num := rec_on a b (λn r, bit0 r + b) @@ -129,17 +129,17 @@ namespace num (H₁ : P zero) (H₂ : ∀ (p : pos_num), P (pos p)) : P a := rec H₁ H₂ a - abbreviation rec_on [protected] {P : num → Type} (a : num) + definition rec_on [protected] {P : num → Type} (a : num) (H₁ : P zero) (H₂ : ∀ (p : pos_num), P (pos p)) : P a := rec H₁ H₂ a - abbreviation succ (a : num) : num := + definition succ (a : num) : num := rec_on a (pos one) (λp, pos (succ p)) - abbreviation pred (a : num) : num := + definition pred (a : num) : num := rec_on a zero (λp, cond (is_one p) zero (pos (pred p))) - abbreviation size (a : num) : num := + definition size (a : num) : num := rec_on a (pos one) (λp, pos (size p)) theorem pred_succ (a : num) : pred (succ a) = a := @@ -151,10 +151,10 @@ namespace num ... = pos (pos_num.pred (pos_num.succ p)) : cond_ff _ _ ... = pos p : {pos_num.pred_succ}) - abbreviation add (a b : num) : num := + definition add (a b : num) : num := rec_on a b (λp_a, rec_on b (pos p_a) (λp_b, pos (pos_num.add p_a p_b))) - abbreviation mul (a b : num) : num := + definition mul (a b : num) : num := rec_on a zero (λp_a, rec_on b zero (λp_b, pos (pos_num.mul p_a p_b))) infixl `+` := add diff --git a/library/data/prod.lean b/library/data/prod.lean index 821e935a7..466ee2378 100644 --- a/library/data/prod.lean +++ b/library/data/prod.lean @@ -12,7 +12,7 @@ open inhabited decidable inductive prod (A B : Type) : Type := mk : A → B → prod A B -abbreviation pair := @prod.mk +definition pair := @prod.mk infixr `×` := prod -- notation for n-ary tuples @@ -22,8 +22,8 @@ namespace prod section parameters {A B : Type} - abbreviation pr1 (p : prod A B) := rec (λ x y, x) p - abbreviation pr2 (p : prod A B) := rec (λ x y, y) p + definition pr1 (p : prod A B) := rec (λ x y, x) p + definition pr2 (p : prod A B) := rec (λ x y, y) p theorem pr1_pair (a : A) (b : B) : pr1 (a, b) = a := rfl diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean index b75faa706..59242d558 100644 --- a/library/data/quotient/basic.lean +++ b/library/data/quotient/basic.lean @@ -19,7 +19,7 @@ namespace quotient -- --------------------- -- TODO: make this a structure -abbreviation is_quotient {A B : Type} (R : A → A → Prop) (abs : A → B) (rep : B → A) : Prop := +definition is_quotient {A B : Type} (R : A → A → Prop) (abs : A → B) (rep : B → A) : Prop := (∀b, abs (rep b) = b) ∧ (∀b, R (rep b) (rep b)) ∧ (∀r s, R r s ↔ (R r r ∧ R s s ∧ abs r = abs s)) @@ -197,10 +197,7 @@ opaque rec rec_constant rec_binary quotient_map quotient_map_binary -- image -- ----- - --- has to be an abbreviation, so that fun_image_definition below will typecheck outside --- the file -abbreviation image {A B : Type} (f : A → B) := subtype (fun b, ∃a, f a = b) +definition image {A B : Type} (f : A → B) := subtype (fun b, ∃a, f a = b) theorem image_inhabited {A B : Type} (f : A → B) (H : inhabited A) : inhabited (image f) := inhabited.mk (tag (f (default A)) (exists_intro (default A) rfl)) diff --git a/library/data/quotient/util.lean b/library/data/quotient/util.lean index 4f4e59e5c..f3823a52f 100644 --- a/library/data/quotient/util.lean +++ b/library/data/quotient/util.lean @@ -28,7 +28,7 @@ theorem flip_pr2 {A B : Type} (a : A × B) : pr2 (flip a) = pr1 a := rfl theorem flip_flip {A B : Type} (a : A × B) : flip (flip a) = a := prod.destruct a (take x y, rfl) -theorem P_flip {A B : Type} {P : A → B → Prop} {a : A × B} (H : P (pr1 a) (pr2 a)) +theorem P_flip {A B : Type} {P : A → B → Prop} (a : A × B) (H : P (pr1 a) (pr2 a)) : P (pr2 (flip a)) (pr1 (flip a)) := (flip_pr1 a)⁻¹ ▸ (flip_pr2 a)⁻¹ ▸ H diff --git a/library/data/sigma.lean b/library/data/sigma.lean index 2f316d75d..7846a7abf 100644 --- a/library/data/sigma.lean +++ b/library/data/sigma.lean @@ -13,8 +13,8 @@ namespace sigma section parameters {A : Type} {B : A → Type} - abbreviation dpr1 (p : Σ x, B x) : A := rec (λ a b, a) p - abbreviation dpr2 (p : Σ x, B x) : B (dpr1 p) := rec (λ a b, b) p + definition dpr1 (p : Σ x, B x) : A := rec (λ a b, a) p + definition dpr2 (p : Σ x, B x) : B (dpr1 p) := rec (λ a b, b) p theorem dpr1_dpair (a : A) (b : B a) : dpr1 (dpair a b) = a := rfl theorem dpr2_dpair (a : A) (b : B a) : dpr2 (dpair a b) = b := rfl diff --git a/library/data/sum.lean b/library/data/sum.lean index 9ab1ff2f1..28b6ff9b5 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -17,11 +17,11 @@ namespace sum infixr `+`:25 := sum -- conflicts with notation for addition end extra_notation - abbreviation rec_on [protected] {A B : Type} {C : (A ⊎ B) → Type} (s : A ⊎ B) + definition rec_on [protected] {A B : Type} {C : (A ⊎ B) → Type} (s : A ⊎ B) (H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s := rec H1 H2 s - abbreviation cases_on [protected] {A B : Type} {P : (A ⊎ B) → Prop} (s : A ⊎ B) + definition cases_on [protected] {A B : Type} {P : (A ⊎ B) → Prop} (s : A ⊎ B) (H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s := rec H1 H2 s diff --git a/library/data/vector.lean b/library/data/vector.lean index a431a0b94..c7827f44e 100644 --- a/library/data/vector.lean +++ b/library/data/vector.lean @@ -77,7 +77,7 @@ namespace vec -- Concat -- ------ - abbreviation cast_subst {A : Type} {P : A → Type} {a a' : A} (H : a = a') (B : P a) : P a' := + definition cast_subst {A : Type} {P : A → Type} {a a' : A} (H : a = a') (B : P a) : P a' := cast (congr_arg P H) B definition concat {n m : ℕ} (v : vec T n) (w : vec T m) : vec T (n + m) := diff --git a/library/hott/equiv.lean b/library/hott/equiv.lean index 0c68b6f17..8c531013a 100644 --- a/library/hott/equiv.lean +++ b/library/hott/equiv.lean @@ -8,7 +8,7 @@ open path -- Equivalences -- ------------ -abbreviation Sect {A B : Type} (s : A → B) (r : B → A) := Πx : A, r (s x) ≈ x +definition Sect {A B : Type} (s : A → B) (r : B → A) := Πx : A, r (s x) ≈ x -- -- TODO: need better means of declaring structures -- -- TODO: note that Coq allows projections to be declared to be coercions on the fly diff --git a/library/hott/path.lean b/library/hott/path.lean index b85123865..f058147a2 100644 --- a/library/hott/path.lean +++ b/library/hott/path.lean @@ -21,9 +21,9 @@ idpath : path a a namespace path infix `≈` := path notation x `≈` y:50 `:>`:0 A:0 := @path A x y -- TODO: is this right? -abbreviation idp {A : Type} {a : A} := idpath a +definition idp {A : Type} {a : A} := idpath a -abbreviation induction_on [protected] {A : Type} {a b : A} (p : a ≈ b) +definition induction_on [protected] {A : Type} {a b : A} (p : a ≈ b) {C : Π (b : A) (p : a ≈ b), Type} (H : C a (idpath a)) : C b p := path.rec H p @@ -33,7 +33,6 @@ path.rec H p definition concat {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : x ≈ z := path.rec (λu, u) q p --- TODO: should this be an abbreviation? definition inverse {A : Type} {x y : A} (p : x ≈ y) : y ≈ x := path.rec (idpath x) p @@ -185,8 +184,7 @@ induction_on p (take q h, h @ (concat_1p _)) q -- Transport -- --------- --- TODO: keep transparent? -abbreviation transport {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) : P y := +definition transport {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) : P y := path.induction_on p u -- This idiom makes the operation right associative. @@ -195,10 +193,9 @@ notation p `#`:65 x:64 := transport _ p x definition ap ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x ≈ y) : f x ≈ f y := path.induction_on p idp --- TODO: is this better than an alias? Note use of curly brackets -abbreviation ap01 := ap +definition ap01 := ap -abbreviation pointwise_paths {A : Type} {P : A → Type} (f g : Πx, P x) : Type := +definition pointwise_paths {A : Type} {P : A → Type} (f g : Πx, P x) : Type := Πx : A, f x ≈ g x infix `∼` := pointwise_paths diff --git a/library/hott/trunc.lean b/library/hott/trunc.lean index d5c736c34..ea0cc2988 100644 --- a/library/hott/trunc.lean +++ b/library/hott/trunc.lean @@ -30,8 +30,8 @@ definition IsTrunc (n : trunc_index) : Type → Type := trunc_index.rec (λA, Contr A) (λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y))) n -- TODO: in the Coq version, this is notation -abbreviation minus_one := trunc_index.trunc_S trunc_index.minus_two -abbreviation IsHProp := IsTrunc minus_one -abbreviation IsHSet := IsTrunc (trunc_index.trunc_S minus_one) +definition minus_one := trunc_index.trunc_S trunc_index.minus_two +definition IsHProp := IsTrunc minus_one +definition IsHSet := IsTrunc (trunc_index.trunc_S minus_one) prefix `!`:75 := center diff --git a/library/logic/axioms/hilbert.lean b/library/logic/axioms/hilbert.lean index 418b20db9..9f1bcb899 100644 --- a/library/logic/axioms/hilbert.lean +++ b/library/logic/axioms/hilbert.lean @@ -38,7 +38,7 @@ nonempty_imp_inhabited (obtain w Hw, from H, nonempty.intro w) -- the Hilbert epsilon function -- ---------------------------- -definition epsilon {A : Type} {H : nonempty A} (P : A → Prop) : A := +definition epsilon [opaque] {A : Type} {H : nonempty A} (P : A → Prop) : A := let u : {x : A, (∃y, P y) → P x} := strong_indefinite_description P H in elt_of u diff --git a/library/logic/core/connectives.lean b/library/logic/core/connectives.lean index 0b5466697..9a3f06641 100644 --- a/library/logic/core/connectives.lean +++ b/library/logic/core/connectives.lean @@ -119,7 +119,7 @@ namespace iff theorem elim_left {a b : Prop} (H : a ↔ b) : a → b := elim (assume H₁ H₂, H₁) H - abbreviation mp := @elim_left + definition mp := @elim_left theorem elim_right {a b : Prop} (H : a ↔ b) : b → a := elim (assume H₁ H₂, H₂) H diff --git a/library/logic/core/decidable.lean b/library/logic/core/decidable.lean index 85d7ff617..54d5c211b 100644 --- a/library/logic/core/decidable.lean +++ b/library/logic/core/decidable.lean @@ -19,7 +19,7 @@ inr not_false_trivial theorem induction_on [protected] {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C := decidable.rec H1 H2 H -definition rec_on [protected] [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : +definition rec_on [protected] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C := decidable.rec H1 H2 H @@ -96,4 +96,4 @@ decidable_iff_equiv Ha (eq_to_iff H) end decidable -abbreviation decidable_eq (A : Type) := Π (a b : A), decidable (a = b) +definition decidable_eq (A : Type) := Π (a b : A), decidable (a = b) diff --git a/library/logic/core/eq.lean b/library/logic/core/eq.lean index 9cfcc73e8..799851b78 100644 --- a/library/logic/core/eq.lean +++ b/library/logic/core/eq.lean @@ -16,7 +16,7 @@ inductive eq {A : Type} (a : A) : A → Prop := refl : eq a a infix `=` := eq -abbreviation rfl {A : Type} {a : A} := eq.refl a +definition rfl {A : Type} {a : A} := eq.refl a namespace eq theorem id_refl {A : Type} {a : A} (H1 : a = a) : H1 = (eq.refl a) := @@ -102,7 +102,7 @@ assume Ha, H2 (H1 ▸ Ha) -- ne -- -- -definition ne [inline] {A : Type} (a b : A) := ¬(a = b) +definition ne {A : Type} (a b : A) := ¬(a = b) infix `≠` := ne namespace ne diff --git a/library/logic/core/instances.lean b/library/logic/core/instances.lean index 0bfca0075..ed63800b1 100644 --- a/library/logic/core/instances.lean +++ b/library/logic/core/instances.lean @@ -127,10 +127,10 @@ namespace iff_ops postfix `⁻¹`:100 := iff.symm infixr `⬝`:75 := iff.trans infixr `▸`:75 := iff.subst - abbreviation refl := iff.refl - abbreviation symm := @iff.symm - abbreviation trans := @iff.trans - abbreviation subst := @iff.subst - abbreviation mp := @iff.mp + definition refl := iff.refl + definition symm := @iff.symm + definition trans := @iff.trans + definition subst := @iff.subst + definition mp := @iff.mp end iff_ops end relation diff --git a/library/logic/core/prop.lean b/library/logic/core/prop.lean index a43b63d94..404937bce 100644 --- a/library/logic/core/prop.lean +++ b/library/logic/core/prop.lean @@ -4,13 +4,13 @@ import general_notation -definition Prop [inline] := Type.{0} +definition Prop := Type.{0} -- implication -- ----------- -abbreviation imp (a b : Prop) : Prop := a → b +definition imp (a b : Prop) : Prop := a → b -- true and false @@ -24,9 +24,9 @@ false.rec c H inductive true : Prop := intro : true -abbreviation trivial := true.intro +definition trivial := true.intro -abbreviation not (a : Prop) := a → false +definition not (a : Prop) := a → false prefix `¬` := not diff --git a/library/logic/core/quantifiers.lean b/library/logic/core/quantifiers.lean index d96bcd9f8..9b37fa47d 100644 --- a/library/logic/core/quantifiers.lean +++ b/library/logic/core/quantifiers.lean @@ -9,7 +9,7 @@ open inhabited nonempty inductive Exists {A : Type} (P : A → Prop) : Prop := intro : ∀ (a : A), P a → Exists P -abbreviation exists_intro := @Exists.intro +definition exists_intro := @Exists.intro notation `exists` binders `,` r:(scoped P, Exists P) := r notation `∃` binders `,` r:(scoped P, Exists P) := r diff --git a/library/tools/fake_simplifier.lean b/library/tools/fake_simplifier.lean index ca4b09c77..9b5d5b0ce 100644 --- a/library/tools/fake_simplifier.lean +++ b/library/tools/fake_simplifier.lean @@ -4,6 +4,6 @@ open tactic namespace fake_simplifier -- until we have the simplifier... -definition simp : tactic := apply @sorry +definition simp [opaque] : tactic := apply @sorry end fake_simplifier diff --git a/library/tools/helper_tactics.lean b/library/tools/helper_tactics.lean index bda430b3b..f4656e47b 100644 --- a/library/tools/helper_tactics.lean +++ b/library/tools/helper_tactics.lean @@ -12,6 +12,6 @@ import .tactic open tactic namespace helper_tactics - definition apply_refl := apply @eq.refl + definition apply_refl [opaque] := apply @eq.refl tactic_hint apply_refl end helper_tactics diff --git a/library/tools/tactic.lean b/library/tools/tactic.lean index 80c4e0b17..24a21fbe8 100644 --- a/library/tools/tactic.lean +++ b/library/tools/tactic.lean @@ -18,28 +18,28 @@ namespace tactic -- uses them when converting Lean expressions into actual tactic objects. -- The bultin 'by' construct triggers the process of converting a -- a term of type 'tactic' into a tactic that sythesizes a term -definition and_then (t1 t2 : tactic) : tactic := builtin -definition or_else (t1 t2 : tactic) : tactic := builtin -definition append (t1 t2 : tactic) : tactic := builtin -definition interleave (t1 t2 : tactic) : tactic := builtin -definition par (t1 t2 : tactic) : tactic := builtin -definition fixpoint (f : tactic → tactic) : tactic := builtin -definition repeat (t : tactic) : tactic := builtin -definition at_most (t : tactic) (k : num) : tactic := builtin -definition discard (t : tactic) (k : num) : tactic := builtin -definition focus_at (t : tactic) (i : num) : tactic := builtin -definition try_for (t : tactic) (ms : num) : tactic := builtin -definition now : tactic := builtin -definition assumption : tactic := builtin -definition eassumption : tactic := builtin -definition state : tactic := builtin -definition fail : tactic := builtin -definition id : tactic := builtin -definition beta : tactic := builtin -definition apply {B : Type} (b : B) : tactic := builtin -definition unfold {B : Type} (b : B) : tactic := builtin -definition exact {B : Type} (b : B) : tactic := builtin -definition trace (s : string) : tactic := builtin +definition and_then [opaque] (t1 t2 : tactic) : tactic := builtin +definition or_else [opaque] (t1 t2 : tactic) : tactic := builtin +definition append [opaque] (t1 t2 : tactic) : tactic := builtin +definition interleave [opaque] (t1 t2 : tactic) : tactic := builtin +definition par [opaque] (t1 t2 : tactic) : tactic := builtin +definition fixpoint [opaque] (f : tactic → tactic) : tactic := builtin +definition repeat [opaque] (t : tactic) : tactic := builtin +definition at_most [opaque] (t : tactic) (k : num) : tactic := builtin +definition discard [opaque] (t : tactic) (k : num) : tactic := builtin +definition focus_at [opaque] (t : tactic) (i : num) : tactic := builtin +definition try_for [opaque] (t : tactic) (ms : num) : tactic := builtin +definition now [opaque] : tactic := builtin +definition assumption [opaque] : tactic := builtin +definition eassumption [opaque] : tactic := builtin +definition state [opaque] : tactic := builtin +definition fail [opaque] : tactic := builtin +definition id [opaque] : tactic := builtin +definition beta [opaque] : tactic := builtin +definition apply [opaque] {B : Type} (b : B) : tactic := builtin +definition unfold [opaque] {B : Type} (b : B) : tactic := builtin +definition exact [opaque] {B : Type} (b : B) : tactic := builtin +definition trace [opaque] (s : string) : tactic := builtin precedence `;`:200 infixl ; := and_then notation `!` t:max := repeat t diff --git a/src/emacs/lean-company.el b/src/emacs/lean-company.el index 8e1e8daf4..d20c6ef29 100644 --- a/src/emacs/lean-company.el +++ b/src/emacs/lean-company.el @@ -133,7 +133,7 @@ (defun company-lean--need-autocomplete () (not (looking-back (rx (or "theorem" "definition" "lemma" "axiom" "parameter" - "abbreviation" "variable" "hypothesis" "conjecture" + "variable" "hypothesis" "conjecture" "corollary" "open") (+ white) (* (not white)))))) diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 4c2c80f39..11bfd8c41 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -8,7 +8,7 @@ (require 'rx) (defconst lean-keywords - '("import" "abbreviation" "opaque" "transparent" "tactic_hint" "definition" "renaming" + '("import" "opaque" "transparent" "tactic_hint" "definition" "renaming" "inline" "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment" @@ -61,7 +61,7 @@ ;; universe/inductive/theorem... "names" (,(rx symbol-start (group (or "universe" "inductive" "theorem" "axiom" "lemma" "hypothesis" - "abbreviation" "definition" "variable" "parameter")) + "definition" "variable" "parameter")) symbol-end (zero-or-more (or whitespace "(" "{" "[")) (group (zero-or-more (not whitespace)))) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 00777e4a2..c7f0aed59 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -27,9 +27,9 @@ static name g_colon(":"); static name g_assign(":="); static name g_private("[private]"); static name g_protected("[protected]"); -static name g_inline("[inline]"); static name g_instance("[instance]"); static name g_coercion("[coercion]"); +static name g_opaque("[opaque]"); environment universe_cmd(parser & p) { name n = p.check_id_next("invalid universe declaration, identifier expected"); @@ -181,8 +181,8 @@ struct decl_modifiers { } else if (p.curr_is_token(g_protected)) { m_is_protected = true; p.next(); - } else if (p.curr_is_token(g_inline)) { - m_is_opaque = false; + } else if (p.curr_is_token(g_opaque)) { + m_is_opaque = true; p.next(); } else if (p.curr_is_token(g_instance)) { m_is_instance = true; @@ -207,13 +207,13 @@ static void erase_local_binder_info(buffer & ps) { p = update_local(p, binder_info()); } -environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { +environment definition_cmd_core(parser & p, bool is_theorem) { auto n_pos = p.pos(); unsigned start_line = n_pos.first; name n = p.check_id_next("invalid declaration, identifier expected"); decl_modifiers modifiers; name real_n; // real name for this declaration - modifiers.m_is_opaque = _is_opaque; + modifiers.m_is_opaque = is_theorem; buffer ls_buffer; expr type, value; level_param_names ls; @@ -362,13 +362,10 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { return env; } environment definition_cmd(parser & p) { - return definition_cmd_core(p, false, true); -} -environment abbreviation_cmd(parser & p) { - return definition_cmd_core(p, false, false); + return definition_cmd_core(p, false); } environment theorem_cmd(parser & p) { - return definition_cmd_core(p, true, true); + return definition_cmd_core(p, true); } static name g_lparen("("), g_lcurly("{"), g_ldcurly("⦃"), g_lbracket("["); @@ -413,7 +410,6 @@ void register_decl_cmds(cmd_table & r) { add_cmd(r, cmd_info("variable", "declare a new parameter", variable_cmd)); add_cmd(r, cmd_info("axiom", "declare a new axiom", axiom_cmd)); add_cmd(r, cmd_info("definition", "add new definition", definition_cmd)); - add_cmd(r, cmd_info("abbreviation", "add new abbreviation (aka transparent definition)", abbreviation_cmd)); add_cmd(r, cmd_info("theorem", "add new theorem", theorem_cmd)); add_cmd(r, cmd_info("variables", "declare new parameters", variables_cmd)); } diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index c94497ac3..4b5f95756 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -79,9 +79,9 @@ token_table init_token_table() { char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion", "variables", "[persistent]", "[private]", "[protected]", "[inline]", "[visible]", "[instance]", - "[class]", "[coercion]", "abbreviation", "opaque", "transparent", + "[class]", "[coercion]", "[opaque]", "abbreviation", "opaque", "transparent", "evaluate", "check", "print", "end", "namespace", "section", "import", - "abbreviation", "inductive", "record", "renaming", "extends", "structure", "module", "universe", + "inductive", "record", "renaming", "extends", "structure", "module", "universe", "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context", "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "tactic_hint", "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "#erase_cache", nullptr}; diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 068e2f048..4e9929e02 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -49,7 +49,7 @@ bool has_tactic_decls(environment const & env) { tc.infer(g_and_then_tac_fn).first == g_tac_type >> (g_tac_type >> g_tac_type) && tc.infer(g_or_else_tac_fn).first == g_tac_type >> (g_tac_type >> g_tac_type) && tc.infer(g_repeat_tac_fn).first == g_tac_type >> g_tac_type; - } catch (...) { + } catch (exception &) { return false; } } diff --git a/src/library/typed_expr.cpp b/src/library/typed_expr.cpp index 0081717ac..8418d8d30 100644 --- a/src/library/typed_expr.cpp +++ b/src/library/typed_expr.cpp @@ -20,13 +20,13 @@ std::string const & get_typed_expr_opcode() { /** \brief This macro is used to "enforce" a given type to an expression. - It is equivalent to the abbreviation + It is equivalent to - abbreviation typed_expr (A : Type) (a : A) := a + definition typed_expr (A : Type) (a : A) := a - We use a macro instead of an abbreviation because we want to be able + We use a macro instead of the definition because we want to be able to use in any environment, even one that does not contain the - abbreviation such as typed_expr. + definition such as typed_expr. The macro is also slightly for efficient because we don't need a universe parameter. diff --git a/tests/lean/bug1.lean b/tests/lean/bug1.lean index a25db34d0..6ad8fdfa5 100644 --- a/tests/lean/bug1.lean +++ b/tests/lean/bug1.lean @@ -1,5 +1,5 @@ -definition bool [inline] : Type.{1} := Type.{0} -definition and [inline] (p q : bool) : bool := ∀ c : bool, (p → q → c) → c +definition bool : Type.{1} := Type.{0} +definition and (p q : bool) : bool := ∀ c : bool, (p → q → c) → c infixl `∧`:25 := and variable a : bool diff --git a/tests/lean/calc1.lean b/tests/lean/calc1.lean index 7dabac10d..c784471f7 100644 --- a/tests/lean/calc1.lean +++ b/tests/lean/calc1.lean @@ -1,5 +1,5 @@ variable A : Type.{1} -definition bool [inline] : Type.{1} := Type.{0} +definition bool : Type.{1} := Type.{0} variable eq : A → A → bool infixl `=`:50 := eq axiom subst (P : A → bool) (a b : A) (H1 : a = b) (H2 : P a) : P b diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean index 0bfeb9ecd..89d7cd01c 100644 --- a/tests/lean/run/algebra1.lean +++ b/tests/lean/run/algebra1.lean @@ -1,6 +1,6 @@ import logic -abbreviation Type1 := Type.{1} +definition Type1 := Type.{1} context parameter {A : Type} @@ -21,12 +21,12 @@ namespace algebra inductive add_struct (A : Type) : Type := mk : (A → A → A) → add_struct A - definition mul [inline] {A : Type} {s : mul_struct A} (a b : A) + definition mul {A : Type} {s : mul_struct A} (a b : A) := mul_struct.rec (fun f, f) s a b infixl `*`:75 := mul - definition add [inline] {A : Type} {s : add_struct A} (a b : A) + definition add {A : Type} {s : add_struct A} (a b : A) := add_struct.rec (fun f, f) s a b infixl `+`:65 := add @@ -41,10 +41,10 @@ namespace nat variable add : nat → nat → nat variable mul : nat → nat → nat - definition is_mul_struct [inline] [instance] : algebra.mul_struct nat + definition is_mul_struct [instance] : algebra.mul_struct nat := algebra.mul_struct.mk mul - definition is_add_struct [inline] [instance] : algebra.add_struct nat + definition is_add_struct [instance] : algebra.add_struct nat := algebra.add_struct.mk add definition to_nat (n : num) : nat @@ -57,22 +57,22 @@ namespace semigroup inductive semigroup_struct (A : Type) : Type := mk : Π (mul : A → A → A), is_assoc mul → semigroup_struct A - definition mul [inline] {A : Type} (s : semigroup_struct A) (a b : A) + definition mul {A : Type} (s : semigroup_struct A) (a b : A) := semigroup_struct.rec (fun f h, f) s a b - definition assoc [inline] {A : Type} (s : semigroup_struct A) : is_assoc (mul s) + definition assoc {A : Type} (s : semigroup_struct A) : is_assoc (mul s) := semigroup_struct.rec (fun f h, h) s - definition is_mul_struct [inline] [instance] (A : Type) (s : semigroup_struct A) : mul_struct A + definition is_mul_struct [instance] (A : Type) (s : semigroup_struct A) : mul_struct A := mul_struct.mk (mul s) inductive semigroup : Type := mk : Π (A : Type), semigroup_struct A → semigroup - definition carrier [inline] [coercion] (g : semigroup) + definition carrier [coercion] (g : semigroup) := semigroup.rec (fun c s, c) g - definition is_semigroup [inline] [instance] (g : semigroup) : semigroup_struct (carrier g) + definition is_semigroup [instance] (g : semigroup) : semigroup_struct (carrier g) := semigroup.rec (fun c s, s) g end semigroup @@ -82,23 +82,23 @@ namespace monoid inductive monoid_struct (A : Type) : Type := mk_monoid_struct : Π (mul : A → A → A) (id : A), is_assoc mul → is_id mul id → monoid_struct A - definition mul [inline] {A : Type} (s : monoid_struct A) (a b : A) + definition mul {A : Type} (s : monoid_struct A) (a b : A) := monoid_struct.rec (fun mul id a i, mul) s a b - definition assoc [inline] {A : Type} (s : monoid_struct A) : is_assoc (mul s) + definition assoc {A : Type} (s : monoid_struct A) : is_assoc (mul s) := monoid_struct.rec (fun mul id a i, a) s open semigroup - definition is_semigroup_struct [inline] [instance] (A : Type) (s : monoid_struct A) : semigroup_struct A + definition is_semigroup_struct [instance] (A : Type) (s : monoid_struct A) : semigroup_struct A := semigroup_struct.mk (mul s) (assoc s) inductive monoid : Type := mk_monoid : Π (A : Type), monoid_struct A → monoid - definition carrier [inline] [coercion] (m : monoid) + definition carrier [coercion] (m : monoid) := monoid.rec (fun c s, c) m - definition is_monoid [inline] [instance] (m : monoid) : monoid_struct (carrier m) + definition is_monoid [instance] (m : monoid) : monoid_struct (carrier m) := monoid.rec (fun c s, s) m end monoid end algebra diff --git a/tests/lean/run/basic.lean b/tests/lean/run/basic.lean index 9975e40ee..d23959a23 100644 --- a/tests/lean/run/basic.lean +++ b/tests/lean/run/basic.lean @@ -30,7 +30,7 @@ end check double check double.{1 2} -definition Prop [inline] := Type.{0} +definition Prop := Type.{0} variable eq : Π {A : Type}, A → A → Prop infix `=`:50 := eq @@ -73,4 +73,4 @@ section end check @bla.is_proj2.{1 2} check @bla.is_proj3.{1 2 3} -end bla \ No newline at end of file +end bla diff --git a/tests/lean/run/cat.lean b/tests/lean/run/cat.lean index 334ad154f..02da97756 100644 --- a/tests/lean/run/cat.lean +++ b/tests/lean/run/cat.lean @@ -21,9 +21,9 @@ namespace category section parameters {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor} - abbreviation compose := rec (λ comp id assoc idr idl, comp) Cat - abbreviation id := rec (λ comp id assoc idr idl, id) Cat - abbreviation ID (A : ob) := @id A + definition compose := rec (λ comp id assoc idr idl, comp) Cat + definition id := rec (λ comp id assoc idr idl, id) Cat + definition ID (A : ob) := @id A infixr `∘` := compose diff --git a/tests/lean/run/class5.lean b/tests/lean/run/class5.lean index 007716c1e..13df8edef 100644 --- a/tests/lean/run/class5.lean +++ b/tests/lean/run/class5.lean @@ -4,7 +4,7 @@ namespace algebra inductive mul_struct (A : Type) : Type := mk : (A → A → A) → mul_struct A - definition mul [inline] {A : Type} {s : mul_struct A} (a b : A) + definition mul {A : Type} {s : mul_struct A} (a b : A) := mul_struct.rec (λ f, f) s a b infixl `*`:75 := mul diff --git a/tests/lean/run/class_bug1.lean b/tests/lean/run/class_bug1.lean index ed04648da..38f21fa32 100644 --- a/tests/lean/run/class_bug1.lean +++ b/tests/lean/run/class_bug1.lean @@ -18,8 +18,8 @@ section sec_cat class foo parameters {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor} - abbreviation compose := rec (λ comp id assoc idr idl, comp) Cat - abbreviation id := rec (λ comp id assoc idr idl, id) Cat + definition compose := rec (λ comp id assoc idr idl, comp) Cat + definition id := rec (λ comp id assoc idr idl, id) Cat infixr `∘`:60 := compose inductive is_section {A B : ob} (f : mor A B) : Type := mk : ∀g, g ∘ f = id → is_section f diff --git a/tests/lean/run/class_bug2.lean b/tests/lean/run/class_bug2.lean index 1626422b9..54861322b 100644 --- a/tests/lean/run/class_bug2.lean +++ b/tests/lean/run/class_bug2.lean @@ -18,8 +18,8 @@ section sec_cat class foo parameters {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor} - abbreviation compose := rec (λ comp id assoc idr idl, comp) Cat - abbreviation id := rec (λ comp id assoc idr idl, id) Cat + definition compose := rec (λ comp id assoc idr idl, comp) Cat + definition id := rec (λ comp id assoc idr idl, id) Cat infixr `∘`:60 := compose end sec_cat end category diff --git a/tests/lean/run/class_coe.lean b/tests/lean/run/class_coe.lean index ac3b5633c..b5ede50a2 100644 --- a/tests/lean/run/class_coe.lean +++ b/tests/lean/run/class_coe.lean @@ -49,7 +49,7 @@ check x + 0 namespace foo variable eq {A : Type} : A → A → Prop infixl `=`:50 := eq -abbreviation id (A : Type) (a : A) := a +definition id (A : Type) (a : A) := a notation A `=` B `:` C := @eq C A B check nat_to_int n + nat_to_int m = (n + m) : int end foo diff --git a/tests/lean/run/cody1.lean b/tests/lean/run/cody1.lean index c58e1ffa7..7e4c3d136 100644 --- a/tests/lean/run/cody1.lean +++ b/tests/lean/run/cody1.lean @@ -1,6 +1,6 @@ import logic -abbreviation subsets (P : Type) := P → Prop. +definition subsets (P : Type) := P → Prop. context diff --git a/tests/lean/run/cody2.lean b/tests/lean/run/cody2.lean index 4aa70076e..d18ac0c84 100644 --- a/tests/lean/run/cody2.lean +++ b/tests/lean/run/cody2.lean @@ -1,6 +1,6 @@ import logic open eq -abbreviation subsets (P : Type) := P → Prop. +definition subsets (P : Type) := P → Prop. context diff --git a/tests/lean/run/congr_imp_bug.lean b/tests/lean/run/congr_imp_bug.lean index 46a4ab03d..3b1f7f197 100644 --- a/tests/lean/run/congr_imp_bug.lean +++ b/tests/lean/run/congr_imp_bug.lean @@ -12,7 +12,7 @@ inductive struc {T1 : Type} {T2 : Type} (R1 : T1 → T1 → Prop) (R2 : T2 → T (f : T1 → T2) : Prop := mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → struc R1 R2 f -abbreviation app {T1 : Type} {T2 : Type} {R1 : T1 → T1 → Prop} {R2 : T2 → T2 → Prop} +definition app {T1 : Type} {T2 : Type} {R1 : T1 → T1 → Prop} {R2 : T2 → T2 → Prop} {f : T1 → T2} (C : struc R1 R2 f) {x y : T1} : R1 x y → R2 (f x) (f y) := struc.rec id C x y @@ -21,7 +21,7 @@ inductive struc2 {T1 : Type} {T2 : Type} {T3 : Type} (R1 : T1 → T1 → Prop) mk2 : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) → struc2 R1 R2 R3 f -abbreviation app2 {T1 : Type} {T2 : Type} {T3 : Type} {R1 : T1 → T1 → Prop} +definition app2 {T1 : Type} {T2 : Type} {T3 : Type} {R1 : T1 → T1 → Prop} {R2 : T2 → T2 → Prop} {R3 : T3 → T3 → Prop} {f : T1 → T2 → T3} (C : struc2 R1 R2 R3 f) {x1 y1 : T1} {x2 y2 : T2} : R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) := diff --git a/tests/lean/run/e1.lean b/tests/lean/run/e1.lean index a3496d42b..7f2a97b99 100644 --- a/tests/lean/run/e1.lean +++ b/tests/lean/run/e1.lean @@ -1,4 +1,4 @@ -definition Prop [inline] : Type.{1} := Type.{0} +definition Prop : Type.{1} := Type.{0} variable eq : forall {A : Type}, A → A → Prop variable N : Type.{1} variables a b c : N diff --git a/tests/lean/run/e14.lean b/tests/lean/run/e14.lean index 18d0efcc3..62af072d6 100644 --- a/tests/lean/run/e14.lean +++ b/tests/lean/run/e14.lean @@ -6,8 +6,8 @@ namespace nat end nat open nat inductive list (A : Type) : Type := nil {} : list A, cons : A → list A → list A -abbreviation nil := @list.nil -abbreviation cons := @list.cons +definition nil := @list.nil +definition cons := @list.cons check nil check nil.{1} diff --git a/tests/lean/run/e2.lean b/tests/lean/run/e2.lean index 0b606100f..0d0f059fc 100644 --- a/tests/lean/run/e2.lean +++ b/tests/lean/run/e2.lean @@ -1,2 +1,2 @@ -definition Prop [inline] := Type.{0} +definition Prop := Type.{0} check Prop diff --git a/tests/lean/run/e3.lean b/tests/lean/run/e3.lean index 5190f7e28..9c1b11e03 100644 --- a/tests/lean/run/e3.lean +++ b/tests/lean/run/e3.lean @@ -1,4 +1,4 @@ -definition Prop [inline] := Type.{0} +definition Prop := Type.{0} definition false := ∀x : Prop, x check false @@ -18,4 +18,3 @@ theorem refl {A : Type} (a : A) : a = a theorem subst {A : Type} {P : A -> Prop} {a b : A} (H1 : a = b) (H2 : P a) : P b := @H1 P H2 - diff --git a/tests/lean/run/e4.lean b/tests/lean/run/e4.lean index 5265bad9b..6a0cff2a7 100644 --- a/tests/lean/run/e4.lean +++ b/tests/lean/run/e4.lean @@ -1,4 +1,4 @@ -definition Prop [inline] := Type.{0} +definition Prop := Type.{0} definition false : Prop := ∀x : Prop, x check false @@ -30,4 +30,3 @@ theorem symm {A : Type} {a b : A} (H : a = b) : b = a theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c := subst H2 H1 - diff --git a/tests/lean/run/e5.lean b/tests/lean/run/e5.lean index b893a69f8..65097cec7 100644 --- a/tests/lean/run/e5.lean +++ b/tests/lean/run/e5.lean @@ -1,4 +1,4 @@ -definition Prop [inline] := Type.{0} +definition Prop := Type.{0} definition false : Prop := ∀x : Prop, x check false @@ -37,7 +37,7 @@ succ : nat → nat namespace nat end nat open nat print "using strict implicit arguments" -abbreviation symmetric {A : Type} (R : A → A → Prop) := ∀ ⦃a b⦄, R a b → R b a +definition symmetric {A : Type} (R : A → A → Prop) := ∀ ⦃a b⦄, R a b → R b a check symmetric variable p : nat → nat → Prop @@ -49,7 +49,7 @@ check H1 H2 print "------------" print "using implicit arguments" -abbreviation symmetric2 {A : Type} (R : A → A → Prop) := ∀ {a b}, R a b → R b a +definition symmetric2 {A : Type} (R : A → A → Prop) := ∀ {a b}, R a b → R b a check symmetric2 check symmetric2 p axiom H3 : symmetric2 p @@ -59,7 +59,7 @@ check H3 H4 print "-----------------" print "using strict implicit arguments (ASCII notation)" -abbreviation symmetric3 {A : Type} (R : A → A → Prop) := ∀ {{a b}}, R a b → R b a +definition symmetric3 {A : Type} (R : A → A → Prop) := ∀ {{a b}}, R a b → R b a check symmetric3 check symmetric3 p diff --git a/tests/lean/run/elab_bug1.lean b/tests/lean/run/elab_bug1.lean index 53e80334d..d145f1757 100644 --- a/tests/lean/run/elab_bug1.lean +++ b/tests/lean/run/elab_bug1.lean @@ -11,7 +11,7 @@ open function namespace congruence -- TODO: move this somewhere else -abbreviation reflexive {T : Type} (R : T → T → Type) : Prop := ∀x, R x x +definition reflexive {T : Type} (R : T → T → Type) : Prop := ∀x, R x x -- Congruence classes for unary and binary functions -- ------------------------------------------------- diff --git a/tests/lean/run/group.lean b/tests/lean/run/group.lean index 477b95cc0..4fd03f33a 100644 --- a/tests/lean/run/group.lean +++ b/tests/lean/run/group.lean @@ -26,7 +26,7 @@ definition group_to_struct [instance] (g : group) : group_struct (carrier g) check group_struct -definition mul [inline] {A : Type} {s : group_struct A} (a b : A) : A +definition mul {A : Type} {s : group_struct A} (a b : A) : A := group_struct.rec (λ mul one inv h1 h2 h3, mul) s a b infixl `*`:75 := mul diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean index f2627850f..db7792c78 100644 --- a/tests/lean/run/group2.lean +++ b/tests/lean/run/group2.lean @@ -28,7 +28,7 @@ definition group_to_struct [instance] (g : group) : group_struct (carrier g) check group_struct -definition mul [inline] {A : Type} {s : group_struct A} (a b : A) : A +definition mul {A : Type} {s : group_struct A} (a b : A) : A := group_struct.rec (λ mul one inv h1 h2 h3, mul) s a b infixl `*`:75 := mul @@ -55,7 +55,7 @@ axiom H1 : is_assoc rmul axiom H2 : is_id rmul rone axiom H3 : is_inv rmul rone rinv -definition real_group_struct [inline] [instance] : group_struct pos_real +definition real_group_struct [instance] : group_struct pos_real := group_struct.mk rmul rone rinv H1 H2 H3 variables x y : pos_real diff --git a/tests/lean/run/have1.lean b/tests/lean/run/have1.lean index 799f50c7d..c75858e6a 100644 --- a/tests/lean/run/have1.lean +++ b/tests/lean/run/have1.lean @@ -1,8 +1,8 @@ -abbreviation Prop : Type.{1} := Type.{0} +definition Prop : Type.{1} := Type.{0} variables a b c : Prop axiom Ha : a axiom Hb : b axiom Hc : c check have H1 : a, from Ha, have H2 : a, using H1, from H1, - H2 \ No newline at end of file + H2 diff --git a/tests/lean/run/have2.lean b/tests/lean/run/have2.lean index ef0cb5a18..8e9715277 100644 --- a/tests/lean/run/have2.lean +++ b/tests/lean/run/have2.lean @@ -1,4 +1,4 @@ -abbreviation Prop : Type.{1} := Type.{0} +definition Prop : Type.{1} := Type.{0} variables a b c : Prop axiom Ha : a axiom Hb : b diff --git a/tests/lean/run/have3.lean b/tests/lean/run/have3.lean index 57a81f1f1..d0dbf963b 100644 --- a/tests/lean/run/have3.lean +++ b/tests/lean/run/have3.lean @@ -1,4 +1,4 @@ -abbreviation Prop : Type.{1} := Type.{0} +definition Prop : Type.{1} := Type.{0} variables a b c : Prop axiom Ha : a axiom Hb : b @@ -7,4 +7,4 @@ check have H1 : a, from Ha, then have H2 : a, from H1, then have H3 : a, from H2, then have H4 : a, from H3, - H4 \ No newline at end of file + H4 diff --git a/tests/lean/run/have4.lean b/tests/lean/run/have4.lean index 0c4516639..5fc4eb2be 100644 --- a/tests/lean/run/have4.lean +++ b/tests/lean/run/have4.lean @@ -1,4 +1,4 @@ -abbreviation Prop : Type.{1} := Type.{0} +definition Prop : Type.{1} := Type.{0} variables a b c : Prop axiom Ha : a axiom Hb : b @@ -7,4 +7,4 @@ check have H1 : a, from Ha, then have H2 : a, from H1, have H3 : a, from H2, then have H4 : a, from H3, - H4 \ No newline at end of file + H4 diff --git a/tests/lean/run/have6.lean b/tests/lean/run/have6.lean index df5face1f..d05d03f43 100644 --- a/tests/lean/run/have6.lean +++ b/tests/lean/run/have6.lean @@ -1,4 +1,4 @@ -abbreviation Prop : Type.{1} := Type.{0} +definition Prop : Type.{1} := Type.{0} variable and : Prop → Prop → Prop infixl `∧`:25 := and variable and_intro : forall (a b : Prop), a → b → a ∧ b diff --git a/tests/lean/run/impbug1.lean b/tests/lean/run/impbug1.lean index d4846ccc1..388ec6658 100644 --- a/tests/lean/run/impbug1.lean +++ b/tests/lean/run/impbug1.lean @@ -1,6 +1,6 @@ -- category -abbreviation Prop := Type.{0} +definition Prop := Type.{0} variable eq {A : Type} : A → A → Prop infix `=`:50 := eq @@ -8,7 +8,7 @@ inductive category (ob : Type) (mor : ob → ob → Type) : Type := mk : Π (id : Π (A : ob), mor A A), (Π (A B : ob) (f : mor A A), id A = f) → category ob mor -abbreviation id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat +definition id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat theorem id_left (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) (A : ob) (f : mor A A) : @eq (mor A A) (id ob mor Cat A) f := diff --git a/tests/lean/run/impbug2.lean b/tests/lean/run/impbug2.lean index 8a0663441..23761ead6 100644 --- a/tests/lean/run/impbug2.lean +++ b/tests/lean/run/impbug2.lean @@ -1,6 +1,6 @@ -- category -abbreviation Prop := Type.{0} +definition Prop := Type.{0} variable eq {A : Type} : A → A → Prop infix `=`:50 := eq @@ -8,7 +8,7 @@ inductive category (ob : Type) (mor : ob → ob → Type) : Type := mk : Π (id : Π (A : ob), mor A A), (Π (A B : ob) (f : mor A A), id A = f) → category ob mor -abbreviation id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat +definition id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat variable ob : Type.{1} variable mor : ob → ob → Type.{1} variable Cat : category ob mor diff --git a/tests/lean/run/impbug3.lean b/tests/lean/run/impbug3.lean index d443ce79f..c118563e8 100644 --- a/tests/lean/run/impbug3.lean +++ b/tests/lean/run/impbug3.lean @@ -1,6 +1,6 @@ -- category -abbreviation Prop := Type.{0} +definition Prop := Type.{0} variable eq {A : Type} : A → A → Prop infix `=`:50 := eq @@ -11,7 +11,7 @@ inductive category : Type := mk : Π (id : Π (A : ob), mor A A), (Π (A B : ob) (f : mor A A), id A = f) → category -abbreviation id (Cat : category) := category.rec (λ id idl, id) Cat +definition id (Cat : category) := category.rec (λ id idl, id) Cat variable Cat : category theorem id_left (A : ob) (f : mor A A) : @eq (mor A A) (id Cat A) f := diff --git a/tests/lean/run/impbug4.lean b/tests/lean/run/impbug4.lean index 3ce726f66..a01b0b39a 100644 --- a/tests/lean/run/impbug4.lean +++ b/tests/lean/run/impbug4.lean @@ -1,6 +1,6 @@ -- category -abbreviation Prop := Type.{0} +definition Prop := Type.{0} variable eq {A : Type} : A → A → Prop infix `=`:50 := eq @@ -11,7 +11,7 @@ inductive category : Type := mk : Π (id : Π (A : ob), mor A A), (Π (A B : ob) (f : mor A A), id A = f) → category -abbreviation id (Cat : category) := category.rec (λ id idl, id) Cat +definition id (Cat : category) := category.rec (λ id idl, id) Cat variable Cat : category set_option unifier.computation true diff --git a/tests/lean/run/ind5.lean b/tests/lean/run/ind5.lean index 1e24d829a..7aabee10e 100644 --- a/tests/lean/run/ind5.lean +++ b/tests/lean/run/ind5.lean @@ -1,4 +1,4 @@ -definition Prop [inline] : Type.{1} := Type.{0} +definition Prop : Type.{1} := Type.{0} inductive or (A B : Prop) : Prop := intro_left : A → or A B, diff --git a/tests/lean/run/indimp.lean b/tests/lean/run/indimp.lean index ae3bd5e28..3e124076c 100644 --- a/tests/lean/run/indimp.lean +++ b/tests/lean/run/indimp.lean @@ -1,4 +1,4 @@ -abbreviation Prop := Type.{0} +definition Prop := Type.{0} inductive nat := zero : nat, diff --git a/tests/lean/run/induniv.lean b/tests/lean/run/induniv.lean index 6b3fc73b4..44fdac565 100644 --- a/tests/lean/run/induniv.lean +++ b/tests/lean/run/induniv.lean @@ -32,7 +32,7 @@ section mk_pair : A → B → pair end -definition Prop [inline] := Type.{0} +definition Prop := Type.{0} inductive eq {A : Type} (a : A) : A → Prop := refl : eq a a diff --git a/tests/lean/run/n3.lean b/tests/lean/run/n3.lean index 8498d81fc..e6caeb677 100644 --- a/tests/lean/run/n3.lean +++ b/tests/lean/run/n3.lean @@ -1,4 +1,4 @@ -definition Prop [inline] : Type.{1} := Type.{0} +definition Prop : Type.{1} := Type.{0} variable N : Type.{1} variable and : Prop → Prop → Prop infixr `∧`:35 := and diff --git a/tests/lean/run/n4.lean b/tests/lean/run/n4.lean index fc9b6afb3..c02dbf6a3 100644 --- a/tests/lean/run/n4.lean +++ b/tests/lean/run/n4.lean @@ -1,4 +1,4 @@ -definition Prop [inline] : Type.{1} := Type.{0} +definition Prop : Type.{1} := Type.{0} context variable N : Type.{1} variables a b c : N diff --git a/tests/lean/run/nat_bug.lean b/tests/lean/run/nat_bug.lean index 26f83232c..347424814 100644 --- a/tests/lean/run/nat_bug.lean +++ b/tests/lean/run/nat_bug.lean @@ -5,7 +5,7 @@ open eq inductive nat : Type := zero : nat, succ : nat → nat -abbreviation refl := @eq.refl +definition refl := @eq.refl namespace nat theorem induction_on {P : nat → Prop} (a : nat) (H1 : P zero) (H2 : ∀ (n : nat) (IH : P n), P (succ n)) : P a := nat.rec H1 H2 a diff --git a/tests/lean/run/nat_bug2.lean b/tests/lean/run/nat_bug2.lean index b4315496a..903f3252e 100644 --- a/tests/lean/run/nat_bug2.lean +++ b/tests/lean/run/nat_bug2.lean @@ -6,9 +6,9 @@ zero : nat, succ : nat → nat namespace nat -abbreviation plus (x y : nat) : nat +definition plus (x y : nat) : nat := nat.rec x (λn r, succ r) y -definition to_nat [coercion] [inline] (n : num) : nat +definition to_nat [coercion] (n : num) : nat := num.rec zero (λn, pos_num.rec (succ zero) (λn r, plus r (plus r (succ zero))) (λn r, plus r r) n) n definition add (x y : nat) : nat := plus x y diff --git a/tests/lean/run/nat_bug3.lean b/tests/lean/run/nat_bug3.lean index 6a864c78b..31d17b016 100644 --- a/tests/lean/run/nat_bug3.lean +++ b/tests/lean/run/nat_bug3.lean @@ -6,9 +6,9 @@ zero : nat, succ : nat → nat namespace nat -abbreviation plus (x y : nat) : nat +definition plus (x y : nat) : nat := nat.rec x (λn r, succ r) y -definition to_nat [coercion] [inline] (n : num) : nat +definition to_nat [coercion] (n : num) : nat := num.rec zero (λn, pos_num.rec (succ zero) (λn r, plus r (plus r (succ zero))) (λn r, plus r r) n) n definition add (x y : nat) : nat := plus x y diff --git a/tests/lean/run/nat_coe.lean b/tests/lean/run/nat_coe.lean index 3d54ab464..c3dee868f 100644 --- a/tests/lean/run/nat_coe.lean +++ b/tests/lean/run/nat_coe.lean @@ -15,12 +15,12 @@ coercion of_nat variables a b : nat variables i j : int -abbreviation c1 := a + b +definition c1 := a + b theorem T1 : c1 = nat_add a b := eq.refl _ -abbreviation c2 := i + j +definition c2 := i + j theorem T2 : c2 = int_add i j := eq.refl _ diff --git a/tests/lean/run/over_subst.lean b/tests/lean/run/over_subst.lean index b2be19116..c6cbd9e88 100644 --- a/tests/lean/run/over_subst.lean +++ b/tests/lean/run/over_subst.lean @@ -20,7 +20,7 @@ infixl `+`:65 := add infix `≤`:50 := le axiom add_assoc (a b c : int) : (a + b) + c = a + (b + c) axiom add_le_left {a b : int} (H : a ≤ b) (c : int) : c + a ≤ c + b -abbreviation lt (a b : int) := a + one ≤ b +definition lt (a b : int) := a + one ≤ b infix `<`:50 := lt end int diff --git a/tests/lean/run/simple.lean b/tests/lean/run/simple.lean index b56520927..7aa59a640 100644 --- a/tests/lean/run/simple.lean +++ b/tests/lean/run/simple.lean @@ -1,4 +1,4 @@ -abbreviation Prop : Type.{1} := Type.{0} +definition Prop : Type.{1} := Type.{0} section parameter A : Type @@ -21,4 +21,4 @@ end check subst.{1} check refl.{1} check symm.{1} -check trans.{1} \ No newline at end of file +check trans.{1} diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean index 74e09074d..f14030ec8 100644 --- a/tests/lean/run/sum_bug.lean +++ b/tests/lean/run/sum_bug.lean @@ -15,7 +15,7 @@ namespace sum infixr `+`:25 := sum -abbreviation rec_on {A B : Type} {C : (A + B) → Type} (s : A + B) +definition rec_on {A B : Type} {C : (A + B) → Type} (s : A + B) (H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s := sum.rec H1 H2 s open eq @@ -26,7 +26,7 @@ have H1 : f (inl B a1), from rfl, have H2 : f (inl B a2), from subst H H1, H2 -abbreviation cases_on {A B : Type} {P : (A + B) → Prop} (s : A + B) +definition cases_on {A B : Type} {P : (A + B) → Prop} (s : A + B) (H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s := sum.rec H1 H2 s diff --git a/tests/lean/run/t9.lean b/tests/lean/run/t9.lean index bcda06dc3..da4bcc5c0 100644 --- a/tests/lean/run/t9.lean +++ b/tests/lean/run/t9.lean @@ -1,4 +1,4 @@ -definition bool [inline] : Type.{1} := Type.{0} +definition bool : Type.{1} := Type.{0} definition and (p q : bool) : bool := ∀ c : bool, (p → q → c) → c infixl `∧`:25 := and diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean index 6f49e5468..29947ef4c 100644 --- a/tests/lean/run/tactic23.lean +++ b/tests/lean/run/tactic23.lean @@ -6,17 +6,17 @@ zero : nat, succ : nat → nat namespace nat -definition add [inline] (a b : nat) : nat +definition add (a b : nat) : nat := nat.rec a (λ n r, succ r) b infixl `+`:65 := add -definition one [inline] := succ zero +definition one := succ zero -- Define coercion from num -> nat -- By default the parser converts numerals into a binary representation num -definition pos_num_to_nat [inline] (n : pos_num) : nat +definition pos_num_to_nat (n : pos_num) : nat := pos_num.rec one (λ n r, r + r) (λ n r, r + r + one) n -definition num_to_nat [inline] (n : num) : nat +definition num_to_nat (n : num) : nat := num.rec zero (λ n, pos_num_to_nat n) n coercion num_to_nat diff --git a/tests/lean/run/trans.lean b/tests/lean/run/trans.lean index 41ddf66f7..12c9043d7 100644 --- a/tests/lean/run/trans.lean +++ b/tests/lean/run/trans.lean @@ -3,7 +3,7 @@ -- Author: Leonardo de Moura import logic open eq -abbreviation refl := @eq.refl +definition refl := @eq.refl definition transport {A : Type} {a b : A} {P : A → Type} (p : a = b) (H : P a) : P b := eq.rec H p diff --git a/tests/lean/run/uuu.lean b/tests/lean/run/uuu.lean index a0b8422e5..1657ee492 100644 --- a/tests/lean/run/uuu.lean +++ b/tests/lean/run/uuu.lean @@ -5,14 +5,14 @@ notation `take` binders `,` r:(scoped f, f) := r inductive empty : Type inductive unit : Type := tt : unit -abbreviation tt := @unit.tt +definition tt := @unit.tt inductive nat : Type := O : nat, S : nat → nat inductive paths {A : Type} (a : A) : A → Type := idpath : paths a a -abbreviation idpath := @paths.idpath +definition idpath := @paths.idpath inductive sum (A : Type) (B : Type) : Type := inl : A -> sum A B, @@ -26,7 +26,7 @@ definition ii2 {A : Type} {B : Type} (b : B) := sum.inl A b inductive total2 {T: Type} (P: T → Type) : Type := tpair : Π (t : T) (tp : P t), total2 P -abbreviation tpair := @total2.tpair +definition tpair := @total2.tpair definition pr1 {T : Type} {P : T → Type} (tp : total2 P) : T := total2.rec (λ a b, a) tp @@ -45,9 +45,9 @@ definition tounit {X : Type} : X → unit definition termfun {X : Type} (x : X) : unit → X := λt, x -abbreviation idfun (T : Type) := λt : T, t +definition idfun (T : Type) := λt : T, t -abbreviation funcomp {X : Type} {Y : Type} {Z : Type} (f : X → Y) (g : Y → Z) +definition funcomp {X : Type} {Y : Type} {Z : Type} (f : X → Y) (g : Y → Z) := λx, g (f x) infixl `∘`:60 := funcomp diff --git a/tests/lean/run/whnfinst.lean b/tests/lean/run/whnfinst.lean index f79626431..efacd6e2b 100644 --- a/tests/lean/run/whnfinst.lean +++ b/tests/lean/run/whnfinst.lean @@ -1,7 +1,7 @@ import logic open decidable -abbreviation decidable_bin_rel {A : Type} (R : A → A → Prop) := Πx y, decidable (R x y) +definition decidable_bin_rel {A : Type} (R : A → A → Prop) := Πx y, decidable (R x y) section parameter {A : Type} diff --git a/tests/lean/slow/list_elab2.lean b/tests/lean/slow/list_elab2.lean index 6a77b4758..57989259c 100644 --- a/tests/lean/slow/list_elab2.lean +++ b/tests/lean/slow/list_elab2.lean @@ -20,7 +20,7 @@ inductive list (T : Type) : Type := nil {} : list T, cons : T → list T → list T -abbreviation refl := @eq.refl +definition refl := @eq.refl namespace list diff --git a/tests/lean/slow/nat_bug1.lean b/tests/lean/slow/nat_bug1.lean index 0b0911351..a15172d50 100644 --- a/tests/lean/slow/nat_bug1.lean +++ b/tests/lean/slow/nat_bug1.lean @@ -13,10 +13,10 @@ succ : nat → nat notation `ℕ`:max := nat namespace nat -abbreviation plus (x y : ℕ) : ℕ +definition plus (x y : ℕ) : ℕ := nat.rec x (λ n r, succ r) y -definition to_nat [coercion] [inline] (n : num) : ℕ +definition to_nat [coercion] (n : num) : ℕ := num.rec zero (λ n, pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n print "==================" diff --git a/tests/lean/slow/nat_bug2.lean b/tests/lean/slow/nat_bug2.lean index c50f6c261..561e36fbf 100644 --- a/tests/lean/slow/nat_bug2.lean +++ b/tests/lean/slow/nat_bug2.lean @@ -7,10 +7,10 @@ import logic algebra.binary open tactic binary eq_ops eq open decidable -abbreviation refl := @eq.refl -abbreviation and_intro := @and.intro -abbreviation or_intro_left := @or.intro_left -abbreviation or_intro_right := @or.intro_right +definition refl := @eq.refl +definition and_intro := @and.intro +definition or_intro_left := @or.intro_left +definition or_intro_right := @or.intro_right inductive nat : Type := zero : nat, @@ -20,10 +20,10 @@ namespace nat notation `ℕ`:max := nat -abbreviation plus (x y : ℕ) : ℕ +definition plus (x y : ℕ) : ℕ := nat.rec x (λ n r, succ r) y -definition to_nat [coercion] [inline] (n : num) : ℕ +definition to_nat [coercion] (n : num) : ℕ := num.rec zero (λ n, pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n namespace helper_tactics diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean index 0ceb8de32..a63207e3e 100644 --- a/tests/lean/slow/nat_wo_hints.lean +++ b/tests/lean/slow/nat_wo_hints.lean @@ -15,10 +15,10 @@ succ : nat → nat namespace nat notation `ℕ`:max := nat -abbreviation plus (x y : ℕ) : ℕ +definition plus (x y : ℕ) : ℕ := nat.rec x (λ n r, succ r) y -definition to_nat [coercion] [inline] (n : num) : ℕ +definition to_nat [coercion] (n : num) : ℕ := num.rec zero (λ n, pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n namespace helper_tactics diff --git a/tests/lean/slow/path_groupoids.lean b/tests/lean/slow/path_groupoids.lean index e0a3e7272..2ecc0087a 100644 --- a/tests/lean/slow/path_groupoids.lean +++ b/tests/lean/slow/path_groupoids.lean @@ -6,8 +6,8 @@ notation `assume` binders `,` r:(scoped f, f) := r notation `take` binders `,` r:(scoped f, f) := r -abbreviation id {A : Type} (a : A) := a -abbreviation compose {A : Type} {B : Type} {C : Type} (g : B → C) (f : A → B) := λ x, g (f x) +definition id {A : Type} (a : A) := a +definition compose {A : Type} {B : Type} {C : Type} (g : B → C) (f : A → B) := λ x, g (f x) infixl `∘`:60 := compose -- Path @@ -15,14 +15,14 @@ infixl `∘`:60 := compose inductive path {A : Type} (a : A) : A → Type := idpath : path a a -abbreviation idpath := @path.idpath +definition idpath := @path.idpath infix `≈`:50 := path -- TODO: is this right? notation x `≈` y:50 `:>`:0 A:0 := @path A x y notation `idp`:max := idpath _ -- TODO: can we / should we use `1`? namespace path - abbreviation induction_on {A : Type} {a b : A} (p : a ≈ b) + definition induction_on {A : Type} {a b : A} (p : a ≈ b) {C : Π (b : A) (p : a ≈ b), Type} (H : C a (idpath a)) : C b p := path.rec H p end path @@ -35,7 +35,6 @@ open path definition concat {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : x ≈ z := path.rec (λu, u) q p --- TODO: should this be an abbreviation? definition inverse {A : Type} {x y : A} (p : x ≈ y) : y ≈ x := path.rec (idpath x) p @@ -188,7 +187,7 @@ induction_on p (take q h, h @ (concat_1p _)) q -- --------- -- keep transparent, so transport _ idp p is definitionally equal to p -abbreviation transport {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) : P y := +definition transport {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) : P y := path.induction_on p u definition transport_1 {A : Type} (P : A → Type) {x : A} (u : P x) : transport _ idp u ≈ u := @@ -203,9 +202,9 @@ definition ap ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x ≈ y) : f x ≈ f y path.induction_on p idp -- TODO: is this better than an alias? Note use of curly brackets -abbreviation ap01 := ap +definition ap01 := ap -abbreviation pointwise_paths {A : Type} {P : A → Type} (f g : Πx, P x) : Type := +definition pointwise_paths {A : Type} {P : A → Type} (f g : Πx, P x) : Type := Πx : A, f x ≈ g x infix `∼`:50 := pointwise_paths diff --git a/tests/lean/t4.lean b/tests/lean/t4.lean index f47a0ec90..070048d4b 100644 --- a/tests/lean/t4.lean +++ b/tests/lean/t4.lean @@ -1,4 +1,4 @@ -definition Prop [inline] : Type.{1} := Type.{0} +definition Prop : Type.{1} := Type.{0} variable N : Type.{1} check N variable a : N