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

chore: unused variables

Browse source
This commit is contained in:
Leonardo de Moura 2022-06-07 16:47:04 -07:00
parent 130cc8bbd5
commit c2ddebc193
7 changed files with 34 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Coe.lean
View file

@ -27,11 +27,11 @@ class CoeTail (α : Sort u) (β : Sort v) where
class CoeHTCT (α : Sort u) (β : Sort v) where
coe : α → β
class CoeDep (α : Sort u) (a : α) (β : Sort v) where
class CoeDep (α : Sort u) (_ : α) (β : Sort v) where
coe : β
/- Combines CoeHead, CoeTC, CoeTail, CoeDep -/
class CoeT (α : Sort u) (a : α) (β : Sort v) where
class CoeT (α : Sort u) (_ : α) (β : Sort v) where
coe : β
class CoeFun (α : Sort u) (γ : outParam (α → Sort v)) where

2
src/Init/Control/Basic.lean
View file

@ -208,7 +208,7 @@ instance (m : Type u → Type v) [Pure m] : MonadControlT m m where
restoreM x := pure x
@[inline]
def controlAt (m : Type u → Type v) {n : Type u → Type w} [s1 : MonadControlT m n] [s2 : Bind n] {α : Type u}
def controlAt (m : Type u → Type v) {n : Type u → Type w} [MonadControlT m n] [Bind n] {α : Type u}
(f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) : n α :=
liftWith f >>= restoreM

2
src/Init/Control/Reader.lean
View file

@ -27,7 +27,7 @@ end ReaderT
instance : MonadControl m (ReaderT ρ m) where
stM := id
liftWith f ctx := f fun x => x ctx
restoreM x ctx := x
restoreM x _ := x
instance ReaderT.tryFinally [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) where
tryFinally' x h ctx := tryFinally' (x ctx) (fun a? => h a? ctx)

15
src/Init/Core.lean
View file

@ -149,14 +149,17 @@ def Priority.max : Priority := 8
non-dedicated workers than the number of cores to reduce context switches. -/
def Priority.dedicated : Priority := 9
set_option linter.unusedVariables.funArgs false in
@[noinline, extern "lean_task_spawn"]
protected def spawn {α : Type u} (fn : Unit → α) (prio := Priority.default) : Task α :=
⟨fn ()⟩
set_option linter.unusedVariables.funArgs false in
@[noinline, extern "lean_task_map"]
protected def map {α : Type u} {β : Type v} (f : α → β) (x : Task α) (prio := Priority.default) : Task β :=
⟨f x.get⟩
set_option linter.unusedVariables.funArgs false in
@[noinline, extern "lean_task_bind"]
protected def bind {α : Type u} {β : Type v} (x : Task α) (f : α → Task β) (prio := Priority.default) : Task β :=
⟨(f x.get).get⟩
@ -424,7 +427,7 @@ end Decidable
section
variable {p q : Prop}
@[inline] def decidable_of_decidable_of_iff [hp : Decidable p] (h : p ↔ q) : Decidable q :=
@[inline] def decidable_of_decidable_of_iff [Decidable p] (h : p ↔ q) : Decidable q :=
if hp : p then
isTrue (Iff.mp h hp)
else
@ -501,7 +504,7 @@ abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f :
(motive := fun (inst : Decidable (f x = f y)) => Decidable.casesOn (motive := fun _ => Sort w) inst (fun _ => P) (fun _ => P → P))
(inst (f x) (f y))
(fun h' => False.elim (h' (congrArg f h)))
(fun h' => fun x => x)
(fun _ => fun x => x)
/- Inhabited -/
@ -554,7 +557,7 @@ structure Equivalence {α : Sort u} (r : α → α → Prop) : Prop where
symm : ∀ {x y}, r x y → r y x
trans : ∀ {x y z}, r x y → r y z → r x z
def emptyRelation {α : Sort u} (a₁ a₂ : α) : Prop :=
def emptyRelation {α : Sort u} (_ _ : α) : Prop :=
False
def Subrelation {α : Sort u} (q r : α → α → Prop) :=
@ -576,7 +579,7 @@ def existsOfSubtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (f
variable {α : Type u} {p : α → Prop}
protected theorem eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
| ⟨_, _ ⟩, ⟨_, _⟩, rfl => rfl
| ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a := by
cases a
@ -959,7 +962,7 @@ variable {α : Sort u}
private def rel {s : Setoid α} (q₁ q₂ : Quotient s) : Prop :=
Quotient.liftOn₂ q₁ q₂
(fun a₁ a₂ => a₁ ≈ a₂)
(fun a₁ a₂ b₁ b₂ a₁b₁ a₂b₂ =>
(fun _ _ _ _ a₁b₁ a₂b₂ =>
propext (Iff.intro
(fun a₁a₂ => Setoid.trans (Setoid.symm a₁b₁) (Setoid.trans a₁a₂ a₂b₂))
(fun b₁b₂ => Setoid.trans a₁b₁ (Setoid.trans b₁b₂ (Setoid.symm a₂b₂)))))
@ -1045,7 +1048,7 @@ private def funSetoid (α : Sort u) (β : α → Sort v) : Setoid (∀ (x : α),
private def extfunApp (f : Quotient <| funSetoid α β) (x : α) : β x :=
Quot.liftOn f
(fun (f : ∀ (x : α), β x) => f x)
(fun f₁ f₂ h => h x)
(fun _ _ h => h x)
theorem funext {f₁ f₂ : ∀ (x : α), β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ := by
show extfunApp (Quotient.mk' f₁) = extfunApp (Quotient.mk' f₂)

4
src/Init/Data/Nat/Basic.lean
View file

@ -200,8 +200,8 @@ theorem sub_le (n m : Nat) : n - m ≤ n := by
| succ m ih => apply Nat.le_trans (pred_le (n - m)) ih
theorem sub_lt : ∀ {n m : Nat}, 0 < n → 0 < m → n - m < n
| 0, _, h1, h2 => absurd h1 (Nat.lt_irrefl 0)
| _+1, 0, h1, h2 => absurd h2 (Nat.lt_irrefl 0)
| 0, _, h1, _ => absurd h1 (Nat.lt_irrefl 0)
| _+1, 0, _, h2 => absurd h2 (Nat.lt_irrefl 0)
| n+1, m+1, _, _ =>
Eq.symm (succ_sub_succ_eq_sub n m) ▸
show n - m < succ n from

13
src/Init/Prelude.lean
View file

@ -111,7 +111,7 @@ theorem eq_of_heq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=
have : (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b :=
fun α _ a _ h₁ =>
HEq.rec (motive := fun {β} (b : β) (_ : HEq a b) => (h₂ : Eq α β) → Eq (cast h₂ a) b)
(fun (h₂ : Eq α α) => rfl)
(fun (_ : Eq α α) => rfl)
h₁
this α α a a' h rfl
@ -161,6 +161,7 @@ structure Subtype {α : Sort u} (p : α → Prop) where
val : α
property : p val
set_option linter.unusedVariables.funArgs false in
/-- Gadget for optional parameter support. -/
@[reducible] def optParam (α : Sort u) (default : α) : Sort u := α
@ -385,7 +386,7 @@ instance : Inhabited Nat where
default := Nat.zero
/- For numeric literals notation -/
class OfNat (α : Type u) (n : Nat) where
class OfNat (α : Type u) (_ : Nat) where
ofNat : α
@[defaultInstance 100] /- low prio -/
@ -1073,8 +1074,8 @@ instance {α} : Inhabited (List α) where
protected def List.hasDecEq {α: Type u} [DecidableEq α] : (a b : List α) → Decidable (Eq a b)
| nil, nil => isTrue rfl
| cons _ as, nil => isFalse (fun h => List.noConfusion h)
| nil, cons _ bs => isFalse (fun h => List.noConfusion h)
| cons _ _, nil => isFalse (fun h => List.noConfusion h)
| nil, cons _ _ => isFalse (fun h => List.noConfusion h)
| cons a as, cons b bs =>
match decEq a b with
| isTrue hab =>
@ -2147,7 +2148,7 @@ private def extractImported (scps : List MacroScope) (mainModule : Name) : Name
match beq str "_@" with
| true => { name := p, mainModule := mainModule, imported := assembleParts parts Name.anonymous, scopes := scps }
| false => extractImported scps mainModule p (List.cons n parts)
| n@(Name.num p str _), parts => extractImported scps mainModule p (List.cons n parts)
| n@(Name.num p _ _), parts => extractImported scps mainModule p (List.cons n parts)
| _, _ => panic "Error: unreachable @ extractImported"
private def extractMainModule (scps : List MacroScope) : Name → List Name → MacroScopesView
@ -2155,7 +2156,7 @@ private def extractMainModule (scps : List MacroScope) : Name → List Name →
match beq str "_@" with
| true => { name := p, mainModule := assembleParts parts Name.anonymous, imported := Name.anonymous, scopes := scps }
| false => extractMainModule scps p (List.cons n parts)
| n@(Name.num _ num _), acc => extractImported scps (assembleParts acc Name.anonymous) n List.nil
| n@(Name.num _ _ _), acc => extractImported scps (assembleParts acc Name.anonymous) n List.nil
| _, _ => panic "Error: unreachable @ extractMainModule"
private def extractMacroScopesAux : Name → List MacroScope → MacroScopesView

24
src/Init/WF.lean
View file

@ -30,7 +30,7 @@ variable {α : Sort u} {r : α → α → Prop}
def inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
Acc.recOn (motive := fun (x : α) _ => r y x → Acc r y)
h₁ (fun x₁ ac₁ ih h₂ => ac₁ y h₂) h₂
h₁ (fun _ ac₁ _ h₂ => ac₁ y h₂) h₂
end Acc
@ -51,7 +51,7 @@ variable {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r)
theorem recursion {C : α → Sort v} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a := by
induction (apply hwf a) with
| intro x₁ _ ih => exact h x₁ ih
| intro x₁ _ ih => exact h x₁ ih
theorem induction {C : α → Prop} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a :=
recursion hwf a h
@ -62,11 +62,11 @@ variable (F : ∀ x, (∀ y, r y x → C y) → C x)
set_option codegen false in
def fixF (x : α) (a : Acc r x) : C x := by
induction a with
| intro x₁ _ ih => exact F x₁ ih
| intro x₁ _ ih => exact F x₁ ih
def fixFEq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p)) := by
induction acx with
| intro x r _ => exact rfl
| intro x r _ => exact rfl
end
@ -101,7 +101,7 @@ variable {α : Sort u} {r q : α → α → Prop}
def accessible {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a := by
induction ac with
| intro x _ ih =>
| intro x _ ih =>
apply Acc.intro
intro y h
exact ih y (h₁ h)
@ -145,7 +145,7 @@ def accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
intro y rel
induction rel with
| base a b rab => exact ih a rab
| trans a b c rab rbc ih₁ ih₂ => apply Acc.inv (ih₂ acx ih) rab
| trans a b c rab _ _ ih₂ => apply Acc.inv (ih₂ acx ih) rab
def wf (h : WellFounded r) : WellFounded (TC r) :=
⟨fun a => accessible (apply h a)⟩
@ -216,9 +216,9 @@ variable {ra : α → α → Prop} {rb : β → β → Prop}
def lexAccessible (aca : (a : α) → Acc ra a) (acb : (b : β) → Acc rb b) (a : α) (b : β) : Acc (Lex ra rb) (a, b) := by
induction (aca a) generalizing b with
| intro xa _ iha =>
| intro xa _ iha =>
induction (acb b) with
| intro xb _ ihb =>
| intro xb _ ihb =>
apply Acc.intro (xa, xb)
intro p lt
cases lt with
@ -268,9 +268,9 @@ variable {r : α → α → Prop} {s : ∀ (a : α), β a → β a → Prop}
def lexAccessible {a} (aca : Acc r a) (acb : (a : α) → WellFounded (s a)) (b : β a) : Acc (Lex r s) ⟨a, b⟩ := by
induction aca with
| intro xa _ iha =>
| intro xa _ iha =>
induction (WellFounded.apply (acb xa) b) with
| intro xb _ ihb =>
| intro xb _ ihb =>
apply Acc.intro
intro p lt
cases lt with
@ -313,10 +313,10 @@ variable {r : α → α → Prop} {s : β → β → Prop}
def revLexAccessible {b} (acb : Acc s b) (aca : (a : α) → Acc r a): (a : α) → Acc (RevLex r s) ⟨a, b⟩ := by
induction acb with
| intro xb _ ihb =>
| intro xb _ ihb =>
intro a
induction (aca a) with
| intro xa _ iha =>
| intro xa _ iha =>
apply Acc.intro
intro p lt
cases lt with