michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): definitions are opaque by default

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-17 14:39:05 -07:00
parent 48dbd13eef
commit baf4c01de8
91 changed files with 251 additions and 276 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/algebra/binary.lean
View file

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

10
library/algebra/category.lean
View file

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

18
library/algebra/function.lean
View file

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

22
library/algebra/relation.lean
View file

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

6
library/data/bool.lean
View file

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

30
library/data/int/basic.lean
View file

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

1
library/data/int/order.lean
View file

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

2
library/data/list/basic.lean
View file

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

13
library/data/nat/basic.lean
View file

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

1
library/data/nat/div.lean
View file

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

4
library/data/nat/order.lean
View file

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

1
library/data/nat/sub.lean
View file

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

26
library/data/num.lean
View file

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

6
library/data/prod.lean
View file

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

7
library/data/quotient/basic.lean
View file

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

2
library/data/quotient/util.lean
View file

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

4
library/data/sigma.lean
View file

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

4
library/data/sum.lean
View file

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

2
library/data/vector.lean
View file

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

2
library/hott/equiv.lean
View file

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

13
library/hott/path.lean
View file

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

6
library/hott/trunc.lean
View file

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

2
library/logic/axioms/hilbert.lean
View file

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

2
library/logic/core/connectives.lean
View file

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

4
library/logic/core/decidable.lean
View file

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

4
library/logic/core/eq.lean
View file

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

10
library/logic/core/instances.lean
View file

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

8
library/logic/core/prop.lean
View file

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

2
library/logic/core/quantifiers.lean
View file

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

2
library/tools/fake_simplifier.lean
View file

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

2
library/tools/helper_tactics.lean
View file

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

44
library/tools/tactic.lean
View file

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

2
src/emacs/lean-company.el
View file

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

4
src/emacs/lean-syntax.el
View file

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

18
src/frontends/lean/decl_cmds.cpp
View file

@ -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<expr> & 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<name> 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));
}

4
src/frontends/lean/token_table.cpp
View file

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

2
src/library/tactic/expr_to_tactic.cpp
View file

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

8
src/library/typed_expr.cpp
View file

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

4
tests/lean/bug1.lean
View file

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

2
tests/lean/calc1.lean
View file

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

30
tests/lean/run/algebra1.lean
View file

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

4
tests/lean/run/basic.lean
View file

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

6
tests/lean/run/cat.lean
View file

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

2
tests/lean/run/class5.lean
View file

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

4
tests/lean/run/class_bug1.lean
View file

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

4
tests/lean/run/class_bug2.lean
View file

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

2
tests/lean/run/class_coe.lean
View file

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

2
tests/lean/run/cody1.lean
View file

@ -1,6 +1,6 @@
import logic
abbreviation subsets (P : Type) := P → Prop.
definition subsets (P : Type) := P → Prop.
context

2
tests/lean/run/cody2.lean
View file

@ -1,6 +1,6 @@
import logic
open eq
abbreviation subsets (P : Type) := P → Prop.
definition subsets (P : Type) := P → Prop.
context

4
tests/lean/run/congr_imp_bug.lean
View file

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

2
tests/lean/run/e1.lean
View file

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

4
tests/lean/run/e14.lean
View file

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

2
tests/lean/run/e2.lean
View file

@ -1,2 +1,2 @@
definition Prop [inline] := Type.{0}
definition Prop := Type.{0}
check Prop

3
tests/lean/run/e3.lean
View file

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

3
tests/lean/run/e4.lean
View file

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

8
tests/lean/run/e5.lean
View file

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

2
tests/lean/run/elab_bug1.lean
View file

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

2
tests/lean/run/group.lean
View file

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

4
tests/lean/run/group2.lean
View file

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

4
tests/lean/run/have1.lean
View file

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

2
tests/lean/run/have2.lean
View file

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

4
tests/lean/run/have3.lean
View file

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

4
tests/lean/run/have4.lean
View file

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

2
tests/lean/run/have6.lean
View file

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

4
tests/lean/run/impbug1.lean
View file

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

4
tests/lean/run/impbug2.lean
View file

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

4
tests/lean/run/impbug3.lean
View file

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

4
tests/lean/run/impbug4.lean
View file

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

2
tests/lean/run/ind5.lean
View file

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

2
tests/lean/run/indimp.lean
View file

@ -1,4 +1,4 @@
abbreviation Prop := Type.{0}
definition Prop := Type.{0}
inductive nat :=
zero : nat,

2
tests/lean/run/induniv.lean
View file

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

2
tests/lean/run/n3.lean
View file

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

2
tests/lean/run/n4.lean
View file

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

2
tests/lean/run/nat_bug.lean
View file

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

4
tests/lean/run/nat_bug2.lean
View file

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

4
tests/lean/run/nat_bug3.lean
View file

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

4
tests/lean/run/nat_coe.lean
View file

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

2
tests/lean/run/over_subst.lean
View file

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

4
tests/lean/run/simple.lean
View file

@ -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}
check trans.{1}

4
tests/lean/run/sum_bug.lean
View file

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

2
tests/lean/run/t9.lean
View file

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

8
tests/lean/run/tactic23.lean
View file

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

2
tests/lean/run/trans.lean
View file

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

10
tests/lean/run/uuu.lean
View file

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

2
tests/lean/run/whnfinst.lean
View file

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

2
tests/lean/slow/list_elab2.lean
View file

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

4
tests/lean/slow/nat_bug1.lean
View file

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

12
tests/lean/slow/nat_bug2.lean
View file

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

4
tests/lean/slow/nat_wo_hints.lean
View file

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

15
tests/lean/slow/path_groupoids.lean
View file

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

2
tests/lean/t4.lean
View file

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