From 0c91b3769ea06b4811d15c0abf2f8d11821053a5 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 22 Jan 2021 14:23:55 +0100 Subject: [PATCH] chore: replace `variables` in src/ --- src/Init/Control/Basic.lean | 2 +- src/Init/Control/EState.lean | 4 ++-- src/Init/Control/Except.lean | 6 +++--- src/Init/Control/Option.lean | 2 +- src/Init/Control/State.lean | 6 +++--- src/Init/Control/StateRef.lean | 2 +- src/Init/Core.lean | 30 +++++++++++++-------------- src/Init/Data/Array/Basic.lean | 2 +- src/Init/Data/Array/Subarray.lean | 2 +- src/Init/Data/List/Basic.lean | 2 +- src/Init/Data/List/BasicAux.lean | 2 +- src/Init/Prelude.lean | 10 ++++----- src/Init/System/IO.lean | 4 ++-- src/Init/System/ST.lean | 2 +- src/Init/WF.lean | 32 ++++++++++++++--------------- src/Lean/Data/Options.lean | 2 +- src/Lean/Data/SMap.lean | 2 +- src/Lean/Data/Trie.lean | 2 +- src/Lean/Elab/DeclModifiers.lean | 2 +- src/Lean/Elab/InfoTree.lean | 2 +- src/Lean/Elab/Log.lean | 2 +- src/Lean/LocalContext.lean | 4 ++-- src/Lean/Meta/Basic.lean | 2 +- src/Lean/MetavarContext.lean | 2 +- src/Lean/Parser/Basic.lean | 2 +- src/Lean/ParserCompiler.lean | 4 ++-- src/Lean/Syntax.lean | 2 +- src/Lean/Util/Constructions.lean | 2 +- src/Lean/Util/ForEachExpr.lean | 2 +- src/Lean/Util/MonadCache.lean | 4 ++-- src/Lean/Util/SCC.lean | 4 ++-- src/Lean/Util/Trace.lean | 6 +++--- src/Std/Data/AssocList.lean | 2 +- src/Std/Data/BinomialHeap.lean | 4 ++-- src/Std/Data/DList.lean | 2 +- src/Std/Data/HashMap.lean | 4 ++-- src/Std/Data/HashSet.lean | 4 ++-- src/Std/Data/PersistentArray.lean | 8 ++++---- src/Std/Data/PersistentHashMap.lean | 6 +++--- src/Std/Data/PersistentHashSet.lean | 2 +- src/Std/Data/RBMap.lean | 8 ++++---- src/Std/Data/RBTree.lean | 2 +- 42 files changed, 98 insertions(+), 98 deletions(-) diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean index b242bbd8df..12e26e6319 100644 --- a/src/Init/Control/Basic.lean +++ b/src/Init/Control/Basic.lean @@ -32,7 +32,7 @@ class Alternative (f : Type u → Type v) extends Applicative f : Type (max (u+1 instance (f : Type u → Type v) (α : Type u) [Alternative f] : OrElse (f α) := ⟨Alternative.orElse⟩ -variables {f : Type u → Type v} [Alternative f] {α : Type u} +variable {f : Type u → Type v} [Alternative f] {α : Type u} export Alternative (failure) diff --git a/src/Init/Control/EState.lean b/src/Init/Control/EState.lean index 04dc034f0c..cf63b7f58f 100644 --- a/src/Init/Control/EState.lean +++ b/src/Init/Control/EState.lean @@ -11,7 +11,7 @@ universes u v namespace EStateM -variables {ε σ α : Type u} +variable {ε σ α : Type u} instance [ToString ε] [ToString α] : ToString (Result ε σ α) where toString @@ -27,7 +27,7 @@ end EStateM namespace EStateM -variables {ε σ α β : Type u} +variable {ε σ α β : Type u} /-- Alternative orElse operator that allows to select which exception should be used. The default is to use the first exception since the standard `orElse` uses the second. -/ diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean index 53dba7e209..a5ca4ae4fd 100644 --- a/src/Init/Control/Except.lean +++ b/src/Init/Control/Except.lean @@ -12,7 +12,7 @@ import Init.Control.Id universes u v w u' namespace Except -variables {ε : Type u} +variable {ε : Type u} @[inline] protected def pure {α : Type v} (a : α) : Except ε α := Except.ok a @@ -58,7 +58,7 @@ def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v := namespace ExceptT -variables {ε : Type u} {m : Type u → Type v} [Monad m] +variable {ε : Type u} {m : Type u → Type v} [Monad m] @[inline] protected def pure {α : Type u} (a : α) : ExceptT ε m α := ExceptT.mk <| pure (Except.ok a) @@ -114,7 +114,7 @@ instance (ε) : MonadExceptOf ε (Except ε) where tryCatch := Except.tryCatch namespace MonadExcept -variables {ε : Type u} {m : Type v → Type w} +variable {ε : Type u} {m : Type v → Type w} /-- Alternative orelse operator that allows to select which exception should be used. The default is to use the first exception since the standard `orelse` uses the second. -/ diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean index 38a58762fe..af1dac4aa5 100644 --- a/src/Init/Control/Option.lean +++ b/src/Init/Control/Option.lean @@ -19,7 +19,7 @@ def OptionT (m : Type u → Type v) (α : Type u) : Type v := x namespace OptionT -variables {m : Type u → Type v} [Monad m] {α β : Type u} +variable {m : Type u → Type v} [Monad m] {α β : Type u} @[inline] protected def bind (x : OptionT m α) (f : α → OptionT m β) : OptionT m β := id (α := m (Option β)) do match (← x) with diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean index 25c1c66f0e..51a7060de0 100644 --- a/src/Init/Control/State.lean +++ b/src/Init/Control/State.lean @@ -32,8 +32,8 @@ instance {σ α} [Subsingleton σ] [Subsingleton α] : Subsingleton (StateM σ namespace StateT section -variables {σ : Type u} {m : Type u → Type v} -variables [Monad m] {α β : Type u} +variable {σ : Type u} {m : Type u → Type v} +variable [Monad m] {α β : Type u} @[inline] protected def pure (a : α) : StateT σ m α := fun s => pure (a, s) @@ -84,7 +84,7 @@ end end StateT section -variables {σ : Type u} {m : Type u → Type v} +variable {σ : Type u} {m : Type u → Type v} instance [Monad m] : MonadStateOf σ (StateT σ m) where get := StateT.get diff --git a/src/Init/Control/StateRef.lean b/src/Init/Control/StateRef.lean index 09eab326c5..e9c6da9620 100644 --- a/src/Init/Control/StateRef.lean +++ b/src/Init/Control/StateRef.lean @@ -24,7 +24,7 @@ def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := pure a namespace StateRefT' -variables {ω σ : Type} {m : Type → Type} {α : Type} +variable {ω σ : Type} {m : Type → Type} {α : Type} @[inline] protected def lift (x : m α) : StateRefT' ω σ m α := fun _ => x diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 72b352afe3..a1bc024859 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -205,7 +205,7 @@ infix:50 " ≠ " => Ne section Ne variable {α : Sort u} -variables {a b : α} {p : Prop} +variable {a b : α} {p : Prop} theorem Ne.intro (h : a = b → False) : a ≠ b := h @@ -232,7 +232,7 @@ theorem trueNeFalse : ¬True = False := end Ne section -variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ} +variable {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ} theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : a ≅ b) : motive b := @HEq.rec α a (fun b _ => motive b) m β b h @@ -278,7 +278,7 @@ theorem heqOfEqRecEq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : theorem castHEq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a | α, _, rfl, a => HEq.refl a -variables {a b c d : Prop} +variable {a b c d : Prop} theorem iffIffImpliesAndImplies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b → a) := Iff.intro (fun h => And.intro h.mp h.mpr) (fun h => Iff.intro h.left h.right) @@ -338,7 +338,7 @@ instance : Decidable False := isFalse notFalse namespace Decidable -variables {p q : Prop} +variable {p q : Prop} @[macroInline] def byCases {q : Sort u} [dec : Decidable p] (h1 : p → q) (h2 : ¬p → q) : q := match dec with @@ -367,7 +367,7 @@ theorem notAndIffOrNot (p q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] : end Decidable section -variables {p q : Prop} +variable {p q : Prop} @[inline] def decidableOfDecidableOfIff (hp : Decidable p) (h : p ↔ q) : Decidable q := if hp : p then isTrue (Iff.mp h hp) @@ -515,7 +515,7 @@ namespace Subtype def existsOfSubtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (fun x => p x) | ⟨a, h⟩ => ⟨a, h⟩ -variables {α : Type u} {p : α → Prop} +variable {α : Type u} {p : α → Prop} protected theorem eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2 | ⟨x, h1⟩, ⟨_, _⟩, rfl => rfl @@ -537,7 +537,7 @@ end Subtype /- Sum -/ section -variables {α : Type u} {β : Type v} +variable {α : Type u} {β : Type v} instance Sum.inhabitedLeft [h : Inhabited α] : Inhabited (Sum α β) where default := Sum.inl arbitrary @@ -561,7 +561,7 @@ end /- Product -/ section -variables {α : Type u} {β : Type v} +variable {α : Type u} {β : Type v} instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where default := (arbitrary, arbitrary) @@ -634,7 +634,7 @@ instance {α : Sort u} [Setoid α] : HasEquiv α := namespace Setoid -variables {α : Sort u} [Setoid α] +variable {α : Sort u} [Setoid α] theorem refl (a : α) : a ≈ a := (Setoid.iseqv α).refl a @@ -810,8 +810,8 @@ end section universes uA uB uC -variables {α : Sort uA} {β : Sort uB} {φ : Sort uC} -variables [s₁ : Setoid α] [s₂ : Setoid β] +variable {α : Sort uA} {β : Sort uB} {φ : Sort uC} +variable [s₁ : Setoid α] [s₂ : Setoid β] protected abbrev lift₂ (f : α → β → φ) @@ -891,8 +891,8 @@ end Exact section universes uA uB uC -variables {α : Sort uA} {β : Sort uB} -variables [s₁ : Setoid α] [s₂ : Setoid β] +variable {α : Sort uA} {β : Sort uB} +variable [s₁ : Setoid α] [s₂ : Setoid β] protected abbrev recOnSubsingleton₂ {motive : Quotient s₁ → Quotient s₂ → Sort uC} @@ -926,7 +926,7 @@ instance {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)] /- Function extensionality -/ namespace Function -variables {α : Sort u} {β : α → Sort v} +variable {α : Sort u} {β : α → Sort v} def Equiv (f₁ f₂ : ∀ (x : α), β x) : Prop := ∀ x, f₁ x = f₂ x @@ -949,7 +949,7 @@ end Function section open Quotient -variables {α : Sort u} {β : α → Sort v} +variable {α : Sort u} {β : α → Sort v} @[instance] private def funSetoid (α : Sort u) (β : α → Sort v) : Setoid (∀ (x : α), β x) := diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index d24ea52dfe..aab08e656c 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -13,7 +13,7 @@ import Init.Util universes u v w namespace Array -variables {α : Type u} +variable {α : Type u} @[extern "lean_mk_array"] def mkArray {α : Type u} (n : Nat) (v : α) : Array α := { diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean index 7e3472afb7..38a0ed9798 100644 --- a/src/Init/Data/Array/Subarray.lean +++ b/src/Init/Data/Array/Subarray.lean @@ -77,7 +77,7 @@ def all {α : Type u} (p : α → Bool) (as : Subarray α) : Bool := end Subarray namespace Array -variables {α : Type u} +variable {α : Type u} def toSubarray (as : Array α) (start stop : Nat) : Subarray α := if h₂ : stop ≤ as.size then diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 9e3fee7df0..adfa42f3b4 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -10,7 +10,7 @@ open Decidable List universes u v w -variables {α : Type u} {β : Type v} {γ : Type w} +variable {α : Type u} {β : Type v} {γ : Type w} namespace List diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean index a9eeea0127..af6f411116 100644 --- a/src/Init/Data/List/BasicAux.lean +++ b/src/Init/Data/List/BasicAux.lean @@ -13,7 +13,7 @@ namespace List /- The following functions can't be defined at `init.data.list.basic`, because they depend on `init.util`, and `init.util` depends on `init.data.list.basic`. -/ -variables {α : Type u} +variable {α : Type u} def get! [Inhabited α] : Nat → List α → α | 0, a::as => a diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index d6458c4469..c290c7e540 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1237,7 +1237,7 @@ instance (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptOf ε m] : tryCatch := tryCatchThe ε namespace MonadExcept -variables {ε : Type u} {m : Type v → Type w} +variable {ε : Type u} {m : Type v → Type w} @[inline] protected def orelse [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) : m α := tryCatch t₁ fun _ => t₂ @@ -1262,7 +1262,7 @@ instance (ρ : Type u) (m : Type u → Type v) (α : Type u) [Inhabited (m α)] namespace ReaderT section -variables {ρ : Type u} {m : Type u → Type v} {α : Type u} +variable {ρ : Type u} {m : Type u → Type v} {α : Type u} instance : MonadLift m (ReaderT ρ m) where monadLift x := fun _ => x @@ -1274,7 +1274,7 @@ instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (ReaderT ρ m) where end section -variables {ρ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} +variable {ρ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} @[inline] protected def read : ReaderT ρ m ρ := pure @@ -1410,7 +1410,7 @@ inductive Result (ε σ α : Type u) where | ok : α → σ → Result ε σ α | error : ε → σ → Result ε σ α -variables {ε σ α : Type u} +variable {ε σ α : Type u} instance [Inhabited ε] [Inhabited σ] : Inhabited (Result ε σ α) where default := Result.error arbitrary arbitrary @@ -1422,7 +1422,7 @@ def EStateM (ε σ α : Type u) := σ → Result ε σ α namespace EStateM -variables {ε σ α β : Type u} +variable {ε σ α β : Type u} instance [Inhabited ε] : Inhabited (EStateM ε σ α) where default := fun s => Result.error arbitrary s diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 2302ea8776..1a7999c9bd 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -186,7 +186,7 @@ def fopenFlags (m : FS.Mode) (b : Bool) : String := end Prim namespace FS -variables [Monad m] [MonadLiftT IO m] +variable [Monad m] [MonadLiftT IO m] def Handle.mk (s : String) (Mode : Mode) (bin : Bool := true) : m Handle := liftM (Prim.Handle.mk s (Prim.fopenFlags Mode bin)) @@ -269,7 +269,7 @@ end Stream end FS section -variables [Monad m] [MonadLiftT IO m] +variable [Monad m] [MonadLiftT IO m] def getStdin : m FS.Stream := liftM Prim.getStdin def getStdout : m FS.Stream := liftM Prim.getStdout diff --git a/src/Init/System/ST.lean b/src/Init/System/ST.lean index cad11f39bf..ead573caee 100644 --- a/src/Init/System/ST.lean +++ b/src/Init/System/ST.lean @@ -97,7 +97,7 @@ def Ref.modifyGet {σ α β : Type} (r : Ref σ α) (f : α → β × α) : ST end Prim section -variables {σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST σ) m] +variable {σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST σ) m] @[inline] def mkRef {α : Type} (a : α) : m (Ref σ α) := liftM <| Prim.mkRef a @[inline] def Ref.get {α : Type} (r : Ref σ α) : m α := liftM <| Prim.Ref.get r diff --git a/src/Init/WF.lean b/src/Init/WF.lean index c3ccde21e3..5ffd434127 100644 --- a/src/Init/WF.lean +++ b/src/Init/WF.lean @@ -26,7 +26,7 @@ abbrev Acc.ndrecOn.{u1, u2} {α : Sort u2} {r : α → α → Prop} {C : α → Acc.rec (motive := fun α _ => C α) m n namespace Acc -variables {α : Sort u} {r : α → α → Prop} +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) @@ -47,7 +47,7 @@ def apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : wf (fun p => p) a section -variables {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r) +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 @@ -69,7 +69,7 @@ def fixFEq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y end -variables {α : Sort u} {C : α → Sort v} {r : α → α → Prop} +variable {α : Sort u} {C : α → Sort v} {r : α → α → Prop} -- Well-founded fixpoint def fix (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x := @@ -93,7 +93,7 @@ def emptyWf {α : Sort u} : WellFounded (@emptyRelation α) := by -- Subrelation of a well-founded relation is well-founded namespace Subrelation -variables {α : Sort u} {r q : α → α → Prop} +variable {α : Sort u} {r q : α → α → Prop} def accessible {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a := by induction ac with @@ -108,7 +108,7 @@ end Subrelation -- The inverse image of a well-founded relation is well-founded namespace InvImage -variables {α : Sort u} {β : Sort v} {r : β → β → Prop} +variable {α : Sort u} {β : Sort v} {r : β → β → Prop} private def accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x = b → Acc (InvImage r f) x := by induction ac with @@ -128,7 +128,7 @@ end InvImage -- The transitive closure of a well-founded relation is well-founded namespace TC -variables {α : Sort u} {r : α → α → Prop} +variable {α : Sort u} {r : α → α → Prop} def accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by induction ac with @@ -180,7 +180,7 @@ namespace Prod open WellFounded section -variables {α : Type u} {β : Type v} +variable {α : Type u} {β : Type v} variable (ra : α → α → Prop) variable (rb : β → β → Prop) @@ -196,8 +196,8 @@ end section -variables {α : Type u} {β : Type v} -variables {ra : α → α → Prop} {rb : β → β → Prop} +variable {α : Type u} {β : Type v} +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 @@ -235,7 +235,7 @@ end Prod namespace PSigma section -variables {α : Sort u} {β : α → Sort v} +variable {α : Sort u} {β : α → Sort v} variable (r : α → α → Prop) variable (s : ∀ a, β a → β a → Prop) @@ -246,8 +246,8 @@ inductive Lex : PSigma β → PSigma β → Prop where end section -variables {α : Sort u} {β : α → Sort v} -variables {r : α → α → Prop} {s : ∀ (a : α), β a → β a → Prop} +variable {α : Sort u} {β : α → Sort v} +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 generalizing b with @@ -266,7 +266,7 @@ def lexWf (ha : WellFounded r) (hb : (x : α) → WellFounded (s x)) : WellFound end section -variables {α : Sort u} {β : Sort v} +variable {α : Sort u} {β : Sort v} def lexNdep (r : α → α → Prop) (s : β → β → Prop) := Lex r (fun a => s) @@ -276,7 +276,7 @@ def lexNdepWf {r : α → α → Prop} {s : β → β → Prop} (ha : WellFound end section -variables {α : Sort u} {β : Sort v} +variable {α : Sort u} {β : Sort v} -- Reverse lexicographical order based on r and s inductive RevLex (r : α → α → Prop) (s : β → β → Prop) : @PSigma α (fun a => β) → @PSigma α (fun a => β) → Prop where @@ -286,8 +286,8 @@ end section open WellFounded -variables {α : Sort u} {β : Sort v} -variables {r : α → α → Prop} {s : β → β → Prop} +variable {α : Sort u} {β : Sort v} +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 diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean index 59342b335e..4fe2e5ebac 100644 --- a/src/Lean/Data/Options.lean +++ b/src/Lean/Data/Options.lean @@ -105,7 +105,7 @@ export MonadOptions (getOptions) instance (m n) [MonadLift m n] [MonadOptions m] : MonadOptions n where getOptions := liftM (getOptions : m _) -variables {m} [Monad m] [MonadOptions m] +variable {m} [Monad m] [MonadOptions m] def getBoolOption (k : Name) (defValue := false) : m Bool := do let opts ← getOptions diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean index 4714b56541..475ac44609 100644 --- a/src/Lean/Data/SMap.lean +++ b/src/Lean/Data/SMap.lean @@ -33,7 +33,7 @@ structure SMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where map₂ : PHashMap α β := {} namespace SMap -variables {α : Type u} {β : Type v} [BEq α] [Hashable α] +variable {α : Type u} {β : Type v} [BEq α] [Hashable α] instance : Inhabited (SMap α β) := ⟨{}⟩ def empty : SMap α β := {} diff --git a/src/Lean/Data/Trie.lean b/src/Lean/Data/Trie.lean index c95446cc78..518fee135d 100644 --- a/src/Lean/Data/Trie.lean +++ b/src/Lean/Data/Trie.lean @@ -16,7 +16,7 @@ inductive Trie (α : Type) where | Node : Option α → RBNode Char (fun _ => Trie α) → Trie α namespace Trie -variables {α : Type} +variable {α : Type} def empty : Trie α := ⟨none, RBNode.leaf⟩ diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index 1efd09c81f..e689a46440 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -80,7 +80,7 @@ def expandOptDocComment? [Monad m] [MonadError m] (optDocComment : Syntax) : m ( section Methods -variables [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] +variable [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] def elabModifiers (stx : Syntax) : m Modifiers := do let docCommentStx := stx[0] diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean index 72b4bed239..a7901c8903 100644 --- a/src/Lean/Elab/InfoTree.lean +++ b/src/Lean/Elab/InfoTree.lean @@ -164,7 +164,7 @@ partial def InfoTree.format (tree : InfoTree) (cinfo? : Option ContextInfo := no return f!"{← i.format cinfo}{Std.Format.nestD <| Std.Format.prefixJoin "\n" (← cs.toList.mapM fun c => format c cinfo?)}" section -variables [Monad m] [MonadInfoTree m] +variable [Monad m] [MonadInfoTree m] @[inline] private def modifyInfoTrees (f : PersistentArray InfoTree → PersistentArray InfoTree) : m Unit := modifyInfoState fun s => { s with trees := f s.trees } diff --git a/src/Lean/Elab/Log.lean b/src/Lean/Elab/Log.lean index 3000688408..2cad5b6fe8 100644 --- a/src/Lean/Elab/Log.lean +++ b/src/Lean/Elab/Log.lean @@ -27,7 +27,7 @@ instance (m n) [MonadLift m n] [MonadLog m] : MonadLog n where getFileName := liftM (getFileName : m _) logMessage := fun msg => liftM (logMessage msg : m _ ) -variables {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] +variable {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] def getRefPos : m String.Pos := do let ref ← MonadLog.getRef diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean index a3fa426360..c9d48926d2 100644 --- a/src/Lean/LocalContext.lean +++ b/src/Lean/LocalContext.lean @@ -256,7 +256,7 @@ def getAt! (lctx : LocalContext) (i : Nat) : Option LocalDecl := section universes u v -variables {m : Type u → Type v} [Monad m] +variable {m : Type u → Type v} [Monad m] variable {β : Type u} @[specialize] def foldlM (lctx : LocalContext) (f : β → LocalDecl → m β) (init : β) (start : Nat := 0) : m β := @@ -338,7 +338,7 @@ def mkForall (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr := section universes u -variables {m : Type → Type u} [Monad m] +variable {m : Type → Type u} [Monad m] @[inline] def anyM (lctx : LocalContext) (p : LocalDecl → m Bool) : m Bool := lctx.decls.anyM fun d => match d with diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 3243c517c1..eaeceab52a 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -157,7 +157,7 @@ builtin_initialize controlAt MetaM fun runInBase => f fun b c => runInBase $ k b c section Methods -variables {n : Type → Type} [MonadControlT MetaM n] [Monad n] +variable {n : Type → Type} [MonadControlT MetaM n] [Monad n] def getLocalInstances : MetaM LocalInstances := return (← read).localInstances diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 722e178b39..d98ce0a491 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -109,7 +109,7 @@ https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379 - When creating lambda/forall expressions, we need to convert/abstract free variables and convert them to bound variables. Now, suppose we a trying to create a lambda/forall expression by abstracting free -variables `xs` and a term `t[?m]` which contains a metavariable `?m`, +variable `xs` and a term `t[?m]` which contains a metavariable `?m`, and the local context of `?m` contains `xs`. The term ``` fun xs => t[?m] diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 859efd38fe..e5f8b27469 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1865,7 +1865,7 @@ end Parser namespace Syntax section -variables {β : Type} {m : Type → Type} [Monad m] +variable {β : Type} {m : Type → Type} [Monad m] @[inline] def foldArgsM (s : Syntax) (f : Syntax → β → m β) (b : β) : m β := s.getArgs.foldlM (flip f) b diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index b9c8f51845..2404605ba7 100644 --- a/src/Lean/ParserCompiler.lean +++ b/src/Lean/ParserCompiler.lean @@ -34,7 +34,7 @@ def replaceParserTy {α} (ctx : Context α) (e : Expr) : Expr := section open Meta -variables {α} (ctx : Context α) (force : Bool := false) in +variable {α} (ctx : Context α) (force : Bool := false) in /-- Translate an expression of type `Parser` into one of type `tyName`, tagging intermediary constants with `ctx.combinatorAttr`. If `force` is `false`, refuse to do so for imported constants. -/ @@ -120,7 +120,7 @@ def compileCategoryParser {α} (ctx : Context α) (declName : Name) (builtin : B ] Attribute.add c' attrName stx -variables {α} (ctx : Context α) in +variable {α} (ctx : Context α) in def compileEmbeddedParsers : ParserDescr → MetaM Unit | ParserDescr.const _ => pure () | ParserDescr.unary _ d => compileEmbeddedParsers d diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean index 759bb31d79..9767458089 100644 --- a/src/Lean/Syntax.lean +++ b/src/Lean/Syntax.lean @@ -297,7 +297,7 @@ class MonadTraverser (m : Type → Type) where namespace MonadTraverser -variables {m : Type → Type} [Monad m] [t : MonadTraverser m] +variable {m : Type → Type} [Monad m] [t : MonadTraverser m] def getCur : m Syntax := Traverser.cur <$> t.st.get def setCur (stx : Syntax) : m Unit := @modify _ _ t.st (fun t => t.setCur stx) diff --git a/src/Lean/Util/Constructions.lean b/src/Lean/Util/Constructions.lean index 5492c2292c..3b384fb98b 100644 --- a/src/Lean/Util/Constructions.lean +++ b/src/Lean/Util/Constructions.lean @@ -16,7 +16,7 @@ namespace Lean @[extern "lean_mk_brec_on"] constant mkBRecOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment @[extern "lean_mk_binduction_on"] constant mkBInductionOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment -variables {m} [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] +variable {m} [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] @[inline] private def adaptFn (f : Environment → Name → Except KernelException Environment) (declName : Name) : m Unit := do match f (← getEnv) declName with diff --git a/src/Lean/Util/ForEachExpr.lean b/src/Lean/Util/ForEachExpr.lean index bcf36bdb13..efd97b5947 100644 --- a/src/Lean/Util/ForEachExpr.lean +++ b/src/Lean/Util/ForEachExpr.lean @@ -13,7 +13,7 @@ may visit the same expression multiple times if they are stored in different mem addresses. Note that the following code is parametric in a monad `m`. -/ -variables {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] +variable {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] namespace ForEachExpr @[specialize] partial def visit (g : Expr → m Bool) (e : Expr) : MonadCacheT Expr Unit m Unit := checkCache e fun _ => do diff --git a/src/Lean/Util/MonadCache.lean b/src/Lean/Util/MonadCache.lean index a21fd10000..8b507d0837 100644 --- a/src/Lean/Util/MonadCache.lean +++ b/src/Lean/Util/MonadCache.lean @@ -56,7 +56,7 @@ def MonadCacheT {ω} (α β : Type) (m : Type → Type) [STWorld ω m] [BEq α] namespace MonadCacheT -variables {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m] +variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m] instance : MonadHashMapCacheAdapter α β (MonadCacheT α β m) where getCache := (get : StateRefT' ..) @@ -79,7 +79,7 @@ def MonadStateCacheT (α β : Type) (m : Type → Type) [BEq α] [Hashable α] : namespace MonadStateCacheT -variables {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m] +variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m] instance : MonadHashMapCacheAdapter α β (MonadStateCacheT α β m) where getCache := (get : StateT ..) diff --git a/src/Lean/Util/SCC.lean b/src/Lean/Util/SCC.lean index 164235fd97..887e2926d9 100644 --- a/src/Lean/Util/SCC.lean +++ b/src/Lean/Util/SCC.lean @@ -14,7 +14,7 @@ namespace Lean.SCC open Std section -variables (α : Type) [BEq α] [Hashable α] +variable (α : Type) [BEq α] [Hashable α] structure Data where index? : Option Nat := none @@ -30,7 +30,7 @@ structure State where abbrev M := StateM (State α) end -variables {α : Type} [BEq α] [Hashable α] +variable {α : Type} [BEq α] [Hashable α] private def getDataOf (a : α) : M α Data := do let s ← get diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index a34d0d9832..c1e5a416e3 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -42,7 +42,7 @@ instance (m n) [MonadLift m n] [MonadTrace m] : MonadTrace n where modifyTraceState := fun f => liftM (modifyTraceState f : m _) getTraceState := liftM (getTraceState : m _) -variables {α : Type} {m : Type → Type} [Monad m] [MonadTrace m] +variable {α : Type} {m : Type → Type} [Monad m] [MonadTrace m] def printTraces {m} [Monad m] [MonadTrace m] [MonadLiftT IO m] : m Unit := do let traceState ← getTraceState @@ -100,7 +100,7 @@ private def getResetTraces : m (PersistentArray TraceElem) := do pure oldTraces section -variables [MonadRef m] [AddMessageContext m] [MonadOptions m] +variable [MonadRef m] [AddMessageContext m] [MonadOptions m] def addTrace (cls : Name) (msg : MessageData) : m Unit := do let ref ← getRef @@ -147,7 +147,7 @@ macro_rules else `(Lean.trace $(quote id.getId) fun _ => ($s : MessageData)) -variables {α : Type} {m : Type → Type} [Monad m] [MonadTrace m] [MonadOptions m] [MonadRef m] +variable {α : Type} {m : Type → Type} [Monad m] [MonadTrace m] [MonadOptions m] [MonadRef m] def withNestedTraces [MonadFinally m] (x : m α) : m α := do let s ← getTraceState diff --git a/src/Std/Data/AssocList.lean b/src/Std/Data/AssocList.lean index b947416c37..c4d1f6eb53 100644 --- a/src/Std/Data/AssocList.lean +++ b/src/Std/Data/AssocList.lean @@ -13,7 +13,7 @@ inductive AssocList (α : Type u) (β : Type v) where deriving Inhabited namespace AssocList -variables {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w} [Monad m] +variable {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w} [Monad m] abbrev empty : AssocList α β := nil diff --git a/src/Std/Data/BinomialHeap.lean b/src/Std/Data/BinomialHeap.lean index 6aa7321530..fede1e6ae9 100644 --- a/src/Std/Data/BinomialHeap.lean +++ b/src/Std/Data/BinomialHeap.lean @@ -19,7 +19,7 @@ inductive Heap (α : Type u) : Type u where abbrev HeapNode (α) := HeapNodeAux α (Heap α) -variables {α : Type u} +variable {α : Type u} def hRank : List (HeapNode α) → Nat | [] => 0 @@ -107,7 +107,7 @@ def BinomialHeap (α : Type u) (lt : α → α → Bool) := { h : Heap α // Wel ⟨Heap.empty, WellFormed.emptyWff⟩ namespace BinomialHeap -variables {α : Type u} {lt : α → α → Bool} +variable {α : Type u} {lt : α → α → Bool} @[inline] def empty : BinomialHeap α lt := mkBinomialHeap α lt diff --git a/src/Std/Data/DList.lean b/src/Std/Data/DList.lean index 1d95287b55..6f9372125d 100644 --- a/src/Std/Data/DList.lean +++ b/src/Std/Data/DList.lean @@ -16,7 +16,7 @@ structure DList (α : Type u) where invariant : ∀ l, apply l = apply [] ++ l namespace DList -variables {α : Type u} +variable {α : Type u} open List def ofList (l : List α) : DList α := diff --git a/src/Std/Data/HashMap.lean b/src/Std/Data/HashMap.lean index 1a588a9813..8c40ac307a 100644 --- a/src/Std/Data/HashMap.lean +++ b/src/Std/Data/HashMap.lean @@ -26,7 +26,7 @@ def mkHashMapImp {α : Type u} {β : Type v} (nbuckets := 8) : HashMapImp α β by rw [Array.sizeMkArrayEq]; cases nbuckets; decide!; apply Nat.zeroLtSucc; done ⟩ } namespace HashMapImp -variables {α : Type u} {β : Type v} +variable {α : Type u} {β : Type v} def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } := ⟨u % n, USize.modnLt _ h⟩ @@ -122,7 +122,7 @@ def mkHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (nbuckets := 8) ⟨ mkHashMapImp nbuckets, WellFormed.mkWff nbuckets ⟩ namespace HashMap -variables {α : Type u} {β : Type v} [BEq α] [Hashable α] +variable {α : Type u} {β : Type v} [BEq α] [Hashable α] instance : Inhabited (HashMap α β) where default := mkHashMap diff --git a/src/Std/Data/HashSet.lean b/src/Std/Data/HashSet.lean index f33497d893..e050c309ca 100644 --- a/src/Std/Data/HashSet.lean +++ b/src/Std/Data/HashSet.lean @@ -25,7 +25,7 @@ def mkHashSetImp {α : Type u} (nbuckets := 8) : HashSetImp α := by rw [Array.sizeMkArrayEq]; cases nbuckets; decide!; apply Nat.zeroLtSucc ⟩ } namespace HashSetImp -variables {α : Type u} +variable {α : Type u} def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } := ⟨u % n, USize.modnLt _ h⟩ @@ -114,7 +114,7 @@ def mkHashSet {α : Type u} [BEq α] [Hashable α] (nbuckets := 8) : HashSet α ⟨ mkHashSetImp nbuckets, WellFormed.mkWff nbuckets ⟩ namespace HashSet -variables {α : Type u} [BEq α] [Hashable α] +variable {α : Type u} [BEq α] [Hashable α] instance : Inhabited (HashSet α) where default := mkHashSet diff --git a/src/Std/Data/PersistentArray.lean b/src/Std/Data/PersistentArray.lean index 2e3f40de76..b6420c5dd4 100644 --- a/src/Std/Data/PersistentArray.lean +++ b/src/Std/Data/PersistentArray.lean @@ -40,7 +40,7 @@ abbrev PArray (α : Type u) := PersistentArray α namespace PersistentArray /- TODO: use proofs for showing that array accesses are not out of bounds. We can do it after we reimplement the tactic framework. -/ -variables {α : Type u} +variable {α : Type u} open Std.PersistentArrayNode def empty : PersistentArray α := {} @@ -181,7 +181,7 @@ def pop (t : PersistentArray α) : PersistentArray α := tailOff := newTailOff } section -variables {m : Type v → Type w} [Monad m] +variable {m : Type v → Type w} [Monad m] variable {β : Type v} @[specialize] private partial def foldlMAux (f : β → α → m β) : PersistentArrayNode α → β → m β @@ -288,7 +288,7 @@ def toList (t : PersistentArray α) : List α := (t.foldl (init := []) fun xs x => x :: xs).reverse section -variables {m : Type → Type w} [Monad m] +variable {m : Type → Type w} [Monad m] @[specialize] partial def anyMAux (p : α → m Bool) : PersistentArrayNode α → m Bool | node cs => cs.anyM fun c => anyMAux p c | leaf vs => vs.anyM p @@ -309,7 +309,7 @@ end !any a fun v => !p v section -variables {m : Type u → Type v} [Monad m] +variable {m : Type u → Type v} [Monad m] variable {β : Type u} @[specialize] partial def mapMAux (f : α → m β) : PersistentArrayNode α → m (PersistentArrayNode β) diff --git a/src/Std/Data/PersistentHashMap.lean b/src/Std/Data/PersistentHashMap.lean index 468d778d95..aa377d1c2c 100644 --- a/src/Std/Data/PersistentHashMap.lean +++ b/src/Std/Data/PersistentHashMap.lean @@ -38,7 +38,7 @@ structure PersistentHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] w abbrev PHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] := PersistentHashMap α β namespace PersistentHashMap -variables {α : Type u} {β : Type v} +variable {α : Type u} {β : Type v} def empty [BEq α] [Hashable α] : PersistentHashMap α β := {} @@ -247,8 +247,8 @@ def erase [BEq α] [Hashable α] : PersistentHashMap α β → α → Persistent { root := n, size := if del then sz - 1 else sz } section -variables {m : Type w → Type w'} [Monad m] -variables {σ : Type w} +variable {m : Type w → Type w'} [Monad m] +variable {σ : Type w} @[specialize] partial def foldlMAux (f : σ → α → β → m σ) : Node α β → σ → m σ | Node.collision keys vals heq, acc => diff --git a/src/Std/Data/PersistentHashSet.lean b/src/Std/Data/PersistentHashSet.lean index 479fea98c1..e5de05e8ca 100644 --- a/src/Std/Data/PersistentHashSet.lean +++ b/src/Std/Data/PersistentHashSet.lean @@ -15,7 +15,7 @@ abbrev PHashSet (α : Type u) [BEq α] [Hashable α] := PersistentHashSet α namespace PersistentHashSet -variables {α : Type u} [BEq α] [Hashable α] +variable {α : Type u} [BEq α] [Hashable α] @[inline] def isEmpty (s : PersistentHashSet α) : Bool := s.set.isEmpty diff --git a/src/Std/Data/RBMap.lean b/src/Std/Data/RBMap.lean index 07d25a63d2..7a5d302fbf 100644 --- a/src/Std/Data/RBMap.lean +++ b/src/Std/Data/RBMap.lean @@ -14,7 +14,7 @@ inductive RBNode (α : Type u) (β : α → Type v) where | node (color : Rbcolor) (lchild : RBNode α β) (key : α) (val : β key) (rchild : RBNode α β) : RBNode α β namespace RBNode -variables {α : Type u} {β : α → Type v} {σ : Type w} +variable {α : Type u} {β : α → Type v} {σ : Type w} open Std.Rbcolor Nat @@ -94,7 +94,7 @@ def isBlack : RBNode α β → Bool section Insert -variables (lt : α → α → Bool) +variable (lt : α → α → Bool) @[specialize] def ins : RBNode α β → (k : α) → β k → RBNode α β | leaf, kx, vx => node red leaf kx vx leaf @@ -166,7 +166,7 @@ partial def appendTrees : RBNode α β → RBNode α β → RBNode α β section Erase -variables (lt : α → α → Bool) +variable (lt : α → α → Bool) @[specialize] def del (x : α) : RBNode α β → RBNode α β | leaf => leaf @@ -235,7 +235,7 @@ instance (α : Type u) (β : Type v) (lt : α → α → Bool) : EmptyCollection ⟨RBMap.empty⟩ namespace RBMap -variables {α : Type u} {β : Type v} {σ : Type w} {lt : α → α → Bool} +variable {α : Type u} {β : Type v} {σ : Type w} {lt : α → α → Bool} def depth (f : Nat → Nat → Nat) (t : RBMap α β lt) : Nat := t.val.depth f diff --git a/src/Std/Data/RBTree.lean b/src/Std/Data/RBTree.lean index e2bd9a4dc8..8facea0ecb 100644 --- a/src/Std/Data/RBTree.lean +++ b/src/Std/Data/RBTree.lean @@ -20,7 +20,7 @@ instance (α : Type u) (lt : α → α → Bool) : EmptyCollection (RBTree α lt ⟨mkRBTree α lt⟩ namespace RBTree -variables {α : Type u} {β : Type v} {lt : α → α → Bool} +variable {α : Type u} {β : Type v} {lt : α → α → Bool} @[inline] def empty : RBTree α lt := RBMap.empty