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

chore(library/init): missing [inline] and remove unnecessary defs

Browse source
This commit is contained in:
Leonardo de Moura 2018-10-17 07:53:30 -07:00
parent 1d0456adf5
commit fa9d6b4ddf
2 changed files with 15 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
library/init/core.lean
View file

@ -403,16 +403,15 @@ infix > := gt
infix ⊇ := superset
infix ⊃ := ssuperset
def bit0 {α : Type u} [s : has_add α] (a : α) : α := a + a
def bit1 {α : Type u} [s₁ : has_one α] [s₂ : has_add α] (a : α) : α := (bit0 a) + 1
@[inline] def bit0 {α : Type u} [s : has_add α] (a : α) : α := a + a
@[inline] def bit1 {α : Type u} [s₁ : has_one α] [s₂ : has_add α] (a : α) : α := (bit0 a) + 1
attribute [pattern] has_zero.zero has_one.one bit0 bit1 has_add.add has_neg.neg
def insert {α : Type u} {γ : Type v} [has_insert α γ] : α → γ → γ :=
has_insert.insert
export has_insert (insert)
/- The empty collection -/
def singleton {α : Type u} {γ : Type v} [has_emptyc γ] [has_insert α γ] (a : α) : γ :=
@[inline] def singleton {α : Type u} {γ : Type v} [has_emptyc γ] [has_insert α γ] (a : α) : γ :=
has_insert.insert a ∅
/- nat basic instances -/
@ -461,8 +460,7 @@ infixr × := prod
class has_sizeof (α : Sort u) :=
(sizeof : α → nat)
def sizeof {α : Sort u} [s : has_sizeof α] : α → nat :=
has_sizeof.sizeof
export has_sizeof (sizeof)
/-
Declare sizeof instances and lemmas for types declared before has_sizeof.
@ -992,16 +990,16 @@ theorem not_or {a b : Prop} : ¬ a → ¬ b → ¬ (a ∨ b)
/- or resolution rulses -/
def resolve_left {a b : Prop} (h : a ∨ b) (na : ¬ a) : b :=
theorem resolve_left {a b : Prop} (h : a ∨ b) (na : ¬ a) : b :=
or.elim h (λ ha, absurd ha na) id
def neg_resolve_left {a b : Prop} (h : ¬ a ∨ b) (ha : a) : b :=
theorem neg_resolve_left {a b : Prop} (h : ¬ a ∨ b) (ha : a) : b :=
or.elim h (λ na, absurd ha na) id
def resolve_right {a b : Prop} (h : a ∨ b) (nb : ¬ b) : a :=
theorem resolve_right {a b : Prop} (h : a ∨ b) (nb : ¬ b) : a :=
or.elim h id (λ hb, absurd hb nb)
def neg_resolve_right {a b : Prop} (h : a ∨ ¬ b) (hb : b) : a :=
theorem neg_resolve_right {a b : Prop} (h : a ∨ ¬ b) (hb : b) : a :=
or.elim h id (λ nb, absurd hb nb)
/- iff simp rules -/
@ -1138,11 +1136,11 @@ end decidable
section
variables {p q : Prop}
def decidable_of_decidable_of_iff (hp : decidable p) (h : p ↔ q) : decidable q :=
@[inline] def decidable_of_decidable_of_iff (hp : decidable p) (h : p ↔ q) : decidable q :=
if hp : p then is_true (iff.mp h hp)
else is_false (iff.mp (not_iff_not_of_iff h) hp)
def decidable_of_decidable_of_eq (hp : decidable p) (h : p = q) : decidable q :=
@[inline] def decidable_of_decidable_of_eq (hp : decidable p) (h : p = q) : decidable q :=
decidable_of_decidable_of_iff hp h.to_iff
@[macro_inline]
@ -1220,6 +1218,7 @@ instance : decidable_eq bool :=
| tt, ff := is_false (ne.symm bool.ff_ne_tt)
| tt, tt := is_true rfl}
@[inline]
def decidable_eq_of_bool_pred {α : Sort u} {p : α → α → bool} (h₁ : is_dec_eq p) (h₂ : is_dec_refl p) : decidable_eq α :=
{dec_eq := λ x y : α,
if hp : p x y = tt then is_true (h₁ hp)

6
library/init/data/char/basic.lean
View file

@ -7,7 +7,7 @@ prelude
import init.data.nat.basic
open nat
@[reducible] def is_valid_char (n : nat) : Prop :=
@[inline, reducible] def is_valid_char (n : nat) : Prop :=
n < 0xd800 ∨ (0xdfff < n ∧ n < 0x110000)
lemma is_valid_char_range_1 (n : nat) (h : n < 0xd800) : is_valid_char n :=
@ -47,10 +47,10 @@ nat.zero_lt_bit0 $ nat.bit0_ne_zero $ nat.bit0_ne_zero $ nat.bit0_ne_zero $
nat.bit0_ne_zero $ nat.bit0_ne_zero $ nat.bit0_ne_zero $ nat.bit0_ne_zero $
nat.bit0_ne_zero $ nat.bit0_ne_zero $ nat.bit0_ne_zero $ nat.bit1_ne_zero 13
@[pattern] def of_nat (n : nat) : char :=
@[inline, pattern] def of_nat (n : nat) : char :=
if h : is_valid_char n then {val := n, valid := h} else {val := 0, valid := or.inl zero_lt_d800}
def to_nat (c : char) : nat :=
@[inline] def to_nat (c : char) : nat :=
c.val
lemma eq_of_veq : ∀ {c d : char}, c.val = d.val → c = d