chore: fix linter errors (#4502)
The linters in Batteries can be used to spot mistakes in Lean. See the message on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Go-to-def.20on.20typeclass.20fields.20and.20type-dependent.20notation/near/442613564). These are the different linters with errors: - unusedArguments: There are many unused instance arguments, especially a redundant `[Monad m]` is very common - checkUnivs: There was a problem with universes in a definition in `Init.Control.StateCps`. I fixed it by adding a `variable` statement for the implicit arguments in the file. - defLemma: many proofs are written as `def` instead of `theorem`, most notably `rfl`. Because `rfl` is used as a match pattern, it must be a def. Is this desirable? The keyword `abbrev` is sometimes used for an alias of a theorem, which also results in a def. I would want to replace it with the `alias` keyword to fix this, but it isn't available. - dupNamespace: I fixed some of these, but left `Tactic.Tactic` and `Parser.Parser` as they are as these seem intended. - unusedHaveSuffices: I cleaned up a few proofs with unused `have` or `suffices` - explicitVarsOfIff: I didn't fix any of these, because that would be a breaking change. - simpNF: I didn't fix any of these, because I think that requires knowing the intended simplification order.
This commit is contained in:
JovanGerb
GitHub
parent
de269060d1
commit
c7c50a8bec
28 changed files with 78 additions and 90 deletions
|
|
@ -131,7 +131,7 @@ protected def adapt {ε' α : Type u} (f : ε → ε') : ExceptT ε m α → Exc
|
|||
end ExceptT
|
||||
|
||||
@[always_inline]
|
||||
instance (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) where
|
||||
instance (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) where
|
||||
throw e := ExceptT.mk <| throwThe ε₁ e
|
||||
tryCatch x handle := ExceptT.mk <| tryCatchThe ε₁ x handle
|
||||
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ import Init.Meta
|
|||
|
||||
open Function
|
||||
|
||||
@[simp] theorem monadLift_self [Monad m] (x : m α) : monadLift x = x :=
|
||||
@[simp] theorem monadLift_self {m : Type u → Type v} (x : m α) : monadLift x = x :=
|
||||
rfl
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@ open Function
|
|||
|
||||
namespace ExceptT
|
||||
|
||||
theorem ext [Monad m] {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
|
||||
theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
|
||||
simp [run] at h
|
||||
assumption
|
||||
|
||||
|
|
@ -50,7 +50,7 @@ theorem run_bind [Monad m] (x : ExceptT ε m α)
|
|||
protected theorem seq_eq {α β ε : Type u} [Monad m] (mf : ExceptT ε m (α → β)) (x : ExceptT ε m α) : mf <*> x = mf >>= fun f => f <$> x :=
|
||||
rfl
|
||||
|
||||
protected theorem bind_pure_comp [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α) : x >>= pure ∘ f = f <$> x := by
|
||||
protected theorem bind_pure_comp [Monad m] (f : α → β) (x : ExceptT ε m α) : x >>= pure ∘ f = f <$> x := by
|
||||
intros; rfl
|
||||
|
||||
protected theorem seqLeft_eq {α β ε : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x <* y = const β <$> x <*> y := by
|
||||
|
|
@ -200,11 +200,11 @@ theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
|
|||
show (f >>= fun g => g <$> x).run s = _
|
||||
simp
|
||||
|
||||
@[simp] theorem run_seqRight [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x *> y).run s = (x.run s >>= fun p => y.run p.2) := by
|
||||
@[simp] theorem run_seqRight [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x *> y).run s = (x.run s >>= fun p => y.run p.2) := by
|
||||
show (x >>= fun _ => y).run s = _
|
||||
simp
|
||||
|
||||
@[simp] theorem run_seqLeft {α β σ : Type u} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x <* y).run s = (x.run s >>= fun p => y.run p.2 >>= fun p' => pure (p.1, p'.2)) := by
|
||||
@[simp] theorem run_seqLeft {α β σ : Type u} [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x <* y).run s = (x.run s >>= fun p => y.run p.2 >>= fun p' => pure (p.1, p'.2)) := by
|
||||
show (x >>= fun a => y >>= fun _ => pure a).run s = _
|
||||
simp
|
||||
|
||||
|
|
|
|||
|
|
@ -67,7 +67,7 @@ instance : MonadExceptOf Unit (OptionT m) where
|
|||
throw := fun _ => OptionT.fail
|
||||
tryCatch := OptionT.tryCatch
|
||||
|
||||
instance (ε : Type u) [Monad m] [MonadExceptOf ε m] : MonadExceptOf ε (OptionT m) where
|
||||
instance (ε : Type u) [MonadExceptOf ε m] : MonadExceptOf ε (OptionT m) where
|
||||
throw e := OptionT.mk <| throwThe ε e
|
||||
tryCatch x handle := OptionT.mk <| tryCatchThe ε x handle
|
||||
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@ instance : MonadControl m (ReaderT ρ m) where
|
|||
restoreM x _ := x
|
||||
|
||||
@[always_inline]
|
||||
instance ReaderT.tryFinally [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) where
|
||||
instance ReaderT.tryFinally [MonadFinally m] : MonadFinally (ReaderT ρ m) where
|
||||
tryFinally' x h ctx := tryFinally' (x ctx) (fun a? => h a? ctx)
|
||||
|
||||
@[reducible] def ReaderM (ρ : Type u) := ReaderT ρ Id
|
||||
|
|
|
|||
|
|
@ -87,7 +87,7 @@ protected def lift {α : Type u} (t : m α) : StateT σ m α :=
|
|||
instance : MonadLift m (StateT σ m) := ⟨StateT.lift⟩
|
||||
|
||||
@[always_inline]
|
||||
instance (σ m) [Monad m] : MonadFunctor m (StateT σ m) := ⟨fun f x s => f (x s)⟩
|
||||
instance (σ m) : MonadFunctor m (StateT σ m) := ⟨fun f x s => f (x s)⟩
|
||||
|
||||
@[always_inline]
|
||||
instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateT σ m) := {
|
||||
|
|
|
|||
|
|
@ -14,16 +14,18 @@ def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type
|
|||
|
||||
namespace StateCpsT
|
||||
|
||||
variable {α σ : Type u} {m : Type u → Type v}
|
||||
|
||||
@[always_inline, inline]
|
||||
def runK {α σ : Type u} {m : Type u → Type v} (x : StateCpsT σ m α) (s : σ) (k : α → σ → m β) : m β :=
|
||||
def runK (x : StateCpsT σ m α) (s : σ) (k : α → σ → m β) : m β :=
|
||||
x _ s k
|
||||
|
||||
@[always_inline, inline]
|
||||
def run {α σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) : m (α × σ) :=
|
||||
def run [Monad m] (x : StateCpsT σ m α) (s : σ) : m (α × σ) :=
|
||||
runK x s (fun a s => pure (a, s))
|
||||
|
||||
@[always_inline, inline]
|
||||
def run' {α σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) : m α :=
|
||||
def run' [Monad m] (x : StateCpsT σ m α) (s : σ) : m α :=
|
||||
runK x s (fun a _ => pure a)
|
||||
|
||||
@[always_inline]
|
||||
|
|
@ -48,29 +50,29 @@ protected def lift [Monad m] (x : m α) : StateCpsT σ m α :=
|
|||
instance [Monad m] : MonadLift m (StateCpsT σ m) where
|
||||
monadLift := StateCpsT.lift
|
||||
|
||||
@[simp] theorem runK_pure {m : Type u → Type v} (a : α) (s : σ) (k : α → σ → m β) : (pure a : StateCpsT σ m α).runK s k = k a s := rfl
|
||||
@[simp] theorem runK_pure (a : α) (s : σ) (k : α → σ → m β) : (pure a : StateCpsT σ m α).runK s k = k a s := rfl
|
||||
|
||||
@[simp] theorem runK_get {m : Type u → Type v} (s : σ) (k : σ → σ → m β) : (get : StateCpsT σ m σ).runK s k = k s s := rfl
|
||||
@[simp] theorem runK_get (s : σ) (k : σ → σ → m β) : (get : StateCpsT σ m σ).runK s k = k s s := rfl
|
||||
|
||||
@[simp] theorem runK_set {m : Type u → Type v} (s s' : σ) (k : PUnit → σ → m β) : (set s' : StateCpsT σ m PUnit).runK s k = k ⟨⟩ s' := rfl
|
||||
@[simp] theorem runK_set (s s' : σ) (k : PUnit → σ → m β) : (set s' : StateCpsT σ m PUnit).runK s k = k ⟨⟩ s' := rfl
|
||||
|
||||
@[simp] theorem runK_modify {m : Type u → Type v} (f : σ → σ) (s : σ) (k : PUnit → σ → m β) : (modify f : StateCpsT σ m PUnit).runK s k = k ⟨⟩ (f s) := rfl
|
||||
@[simp] theorem runK_modify (f : σ → σ) (s : σ) (k : PUnit → σ → m β) : (modify f : StateCpsT σ m PUnit).runK s k = k ⟨⟩ (f s) := rfl
|
||||
|
||||
@[simp] theorem runK_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) (k : α → σ → m β) : (StateCpsT.lift x : StateCpsT σ m α).runK s k = x >>= (k . s) := rfl
|
||||
@[simp] theorem runK_lift [Monad m] (x : m α) (s : σ) (k : α → σ → m β) : (StateCpsT.lift x : StateCpsT σ m α).runK s k = x >>= (k . s) := rfl
|
||||
|
||||
@[simp] theorem runK_monadLift {σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) (k : α → σ → m β)
|
||||
@[simp] theorem runK_monadLift [Monad m] [MonadLiftT n m] (x : n α) (s : σ) (k : α → σ → m β)
|
||||
: (monadLift x : StateCpsT σ m α).runK s k = (monadLift x : m α) >>= (k . s) := rfl
|
||||
|
||||
@[simp] theorem runK_bind_pure {α σ : Type u} [Monad m] (a : α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (pure a >>= f).runK s k = (f a).runK s k := rfl
|
||||
@[simp] theorem runK_bind_pure (a : α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (pure a >>= f).runK s k = (f a).runK s k := rfl
|
||||
|
||||
@[simp] theorem runK_bind_lift {α σ : Type u} [Monad m] (x : m α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ)
|
||||
@[simp] theorem runK_bind_lift [Monad m] (x : m α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ)
|
||||
: (StateCpsT.lift x >>= f).runK s k = x >>= fun a => (f a).runK s k := rfl
|
||||
|
||||
@[simp] theorem runK_bind_get {σ : Type u} [Monad m] (f : σ → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (get >>= f).runK s k = (f s).runK s k := rfl
|
||||
@[simp] theorem runK_bind_get (f : σ → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (get >>= f).runK s k = (f s).runK s k := rfl
|
||||
|
||||
@[simp] theorem runK_bind_set {σ : Type u} [Monad m] (f : PUnit → StateCpsT σ m β) (s s' : σ) (k : β → σ → m γ) : (set s' >>= f).runK s k = (f ⟨⟩).runK s' k := rfl
|
||||
@[simp] theorem runK_bind_set (f : PUnit → StateCpsT σ m β) (s s' : σ) (k : β → σ → m γ) : (set s' >>= f).runK s k = (f ⟨⟩).runK s' k := rfl
|
||||
|
||||
@[simp] theorem runK_bind_modify {σ : Type u} [Monad m] (f : σ → σ) (g : PUnit → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (modify f >>= g).runK s k = (g ⟨⟩).runK (f s) k := rfl
|
||||
@[simp] theorem runK_bind_modify (f : σ → σ) (g : PUnit → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (modify f >>= g).runK s k = (g ⟨⟩).runK (f s) k := rfl
|
||||
|
||||
@[simp] theorem run_eq [Monad m] (x : StateCpsT σ m α) (s : σ) : x.run s = x.runK s (fun a s => pure (a, s)) := rfl
|
||||
|
||||
|
|
|
|||
|
|
@ -34,22 +34,22 @@ protected def lift (x : m α) : StateRefT' ω σ m α :=
|
|||
|
||||
instance [Monad m] : Monad (StateRefT' ω σ m) := inferInstanceAs (Monad (ReaderT _ _))
|
||||
instance : MonadLift m (StateRefT' ω σ m) := ⟨StateRefT'.lift⟩
|
||||
instance (σ m) [Monad m] : MonadFunctor m (StateRefT' ω σ m) := inferInstanceAs (MonadFunctor m (ReaderT _ _))
|
||||
instance (σ m) : MonadFunctor m (StateRefT' ω σ m) := inferInstanceAs (MonadFunctor m (ReaderT _ _))
|
||||
instance [Alternative m] [Monad m] : Alternative (StateRefT' ω σ m) := inferInstanceAs (Alternative (ReaderT _ _))
|
||||
|
||||
@[inline]
|
||||
protected def get [Monad m] [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
|
||||
protected def get [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
|
||||
fun ref => ref.get
|
||||
|
||||
@[inline]
|
||||
protected def set [Monad m] [MonadLiftT (ST ω) m] (s : σ) : StateRefT' ω σ m PUnit :=
|
||||
protected def set [MonadLiftT (ST ω) m] (s : σ) : StateRefT' ω σ m PUnit :=
|
||||
fun ref => ref.set s
|
||||
|
||||
@[inline]
|
||||
protected def modifyGet [Monad m] [MonadLiftT (ST ω) m] (f : σ → α × σ) : StateRefT' ω σ m α :=
|
||||
protected def modifyGet [MonadLiftT (ST ω) m] (f : σ → α × σ) : StateRefT' ω σ m α :=
|
||||
fun ref => ref.modifyGet f
|
||||
|
||||
instance [MonadLiftT (ST ω) m] [Monad m] : MonadStateOf σ (StateRefT' ω σ m) where
|
||||
instance [MonadLiftT (ST ω) m] : MonadStateOf σ (StateRefT' ω σ m) where
|
||||
get := StateRefT'.get
|
||||
set := StateRefT'.set
|
||||
modifyGet := StateRefT'.modifyGet
|
||||
|
|
|
|||
|
|
@ -642,7 +642,7 @@ instance : LawfulBEq String := inferInstance
|
|||
|
||||
/-! # Logical connectives and equality -/
|
||||
|
||||
@[inherit_doc True.intro] def trivial : True := ⟨⟩
|
||||
@[inherit_doc True.intro] theorem trivial : True := ⟨⟩
|
||||
|
||||
theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a :=
|
||||
fun ha => h₂ (h₁ ha)
|
||||
|
|
@ -1173,7 +1173,7 @@ def Prod.lexLt [LT α] [LT β] (s : α × β) (t : α × β) : Prop :=
|
|||
s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)
|
||||
|
||||
instance Prod.lexLtDec
|
||||
[LT α] [LT β] [DecidableEq α] [DecidableEq β]
|
||||
[LT α] [LT β] [DecidableEq α]
|
||||
[(a b : α) → Decidable (a < b)] [(a b : β) → Decidable (a < b)]
|
||||
: (s t : α × β) → Decidable (Prod.lexLt s t) :=
|
||||
fun _ _ => inferInstanceAs (Decidable (_ ∨ _))
|
||||
|
|
|
|||
|
|
@ -184,8 +184,7 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
|
|||
· simp only [h]
|
||||
rw [Nat.div_eq_sub_div (Nat.two_pow_pos w) h, Nat.div_eq_of_lt]
|
||||
· decide
|
||||
· have : BitVec.toNat x < 2^w + 2^w := by simpa [Nat.pow_succ, Nat.mul_two] using x.isLt
|
||||
omega
|
||||
· omega
|
||||
|
||||
@[bv_toNat] theorem getLsb_succ_last (x : BitVec (w + 1)) :
|
||||
x.getLsb w = decide (2 ^ w ≤ x.toNat) := getLsb_last x
|
||||
|
|
@ -331,10 +330,7 @@ theorem toNat_eq_nat (x : BitVec w) (y : Nat)
|
|||
: (x.toNat = y) ↔ (y < 2^w ∧ (x = BitVec.ofNat w y)) := by
|
||||
apply Iff.intro
|
||||
· intro eq
|
||||
simp at eq
|
||||
have lt := x.isLt
|
||||
simp [eq] at lt
|
||||
simp [←eq, lt, x.isLt]
|
||||
simp [←eq, x.isLt]
|
||||
· intro eq
|
||||
simp [Nat.mod_eq_of_lt, eq]
|
||||
|
||||
|
|
@ -1240,11 +1236,7 @@ x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>
|
|||
theorem getLsb_rotateLeftAux_of_le {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
|
||||
(x.rotateLeftAux r).getLsb i = x.getLsb (w - r + i) := by
|
||||
rw [rotateLeftAux, getLsb_or, getLsb_ushiftRight]
|
||||
suffices (x <<< r).getLsb i = false by
|
||||
simp; omega
|
||||
simp only [getLsb_shiftLeft, Bool.and_eq_false_imp, Bool.and_eq_true, decide_eq_true_eq,
|
||||
Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, and_imp]
|
||||
omega
|
||||
simp; omega
|
||||
|
||||
/--
|
||||
Accessing bits in `x.rotateLeft r` the range `[r, w)` is equal to
|
||||
|
|
|
|||
|
|
@ -636,7 +636,7 @@ theorem sub_ediv_of_dvd (a : Int) {b c : Int}
|
|||
have := Int.mul_ediv_cancel 1 H; rwa [Int.one_mul] at this
|
||||
|
||||
@[simp]
|
||||
theorem Int.emod_sub_cancel (x y : Int): (x - y)%y = x%y := by
|
||||
theorem emod_sub_cancel (x y : Int): (x - y)%y = x%y := by
|
||||
by_cases h : y = 0
|
||||
· simp [h]
|
||||
· simp only [Int.emod_def, Int.sub_ediv_of_dvd, Int.dvd_refl, Int.ediv_self h, Int.mul_sub]
|
||||
|
|
|
|||
|
|
@ -583,8 +583,6 @@ theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul
|
|||
have : k ≠ 0 → k + 1 ≠ 1 := by intro h; match k with | 0 => contradiction | k+1 => simp [Nat.succ.injEq]
|
||||
have : ¬ (k == 0) → (k + 1 == 1) = false := fun h => beq_false_of_ne (this (ne_of_beq_false (Bool.of_not_eq_true h)))
|
||||
have : ¬ ((k + 1 == 0) = true) := fun h => absurd (eq_of_beq h) (Nat.succ_ne_zero k)
|
||||
have : (1 == (0 : Nat)) = false := rfl
|
||||
have : (1 == (1 : Nat)) = true := rfl
|
||||
by_cases he : eq = true <;> simp [he, PolyCnstr.mul, PolyCnstr.denote, Poly.denote_le, Poly.denote_eq]
|
||||
<;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply Iff.intro <;> intro h
|
||||
· exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h
|
||||
|
|
|
|||
|
|
@ -740,7 +740,7 @@ prove `p` given any element `x : α`, then `p` holds. Note that it is essential
|
|||
that `p` is a `Prop` here; the version with `p` being a `Sort u` is equivalent
|
||||
to `Classical.choice`.
|
||||
-/
|
||||
protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
|
||||
protected theorem Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
|
||||
match h₁ with
|
||||
| intro a => h₂ a
|
||||
|
||||
|
|
@ -3150,7 +3150,7 @@ instance (ρ : Type u) (m : Type u → Type v) [MonadWithReaderOf ρ m] : MonadW
|
|||
instance {ρ : Type u} {m : Type u → Type v} {n : Type u → Type v} [MonadFunctor m n] [MonadWithReaderOf ρ m] : MonadWithReaderOf ρ n where
|
||||
withReader f := monadMap (m := m) (withTheReader ρ f)
|
||||
|
||||
instance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadWithReaderOf ρ (ReaderT ρ m) where
|
||||
instance {ρ : Type u} {m : Type u → Type v} : MonadWithReaderOf ρ (ReaderT ρ m) where
|
||||
withReader f x := fun ctx => x (f ctx)
|
||||
|
||||
/--
|
||||
|
|
@ -3233,7 +3233,7 @@ def modify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ →
|
|||
of the state. It is equivalent to `get <* modify f` but may be more efficient.
|
||||
-/
|
||||
@[always_inline, inline]
|
||||
def getModify {σ : Type u} {m : Type u → Type v} [MonadState σ m] [Monad m] (f : σ → σ) : m σ :=
|
||||
def getModify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ → σ) : m σ :=
|
||||
modifyGet fun s => (s, f s)
|
||||
|
||||
-- NOTE: The Ordering of the following two instances determines that the top-most `StateT` Monad layer
|
||||
|
|
|
|||
|
|
@ -37,7 +37,7 @@ noncomputable abbrev Acc.ndrecOn.{u1, u2} {α : Sort u2} {r : α → α → Prop
|
|||
namespace Acc
|
||||
variable {α : Sort u} {r : α → α → Prop}
|
||||
|
||||
def inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
|
||||
theorem inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
|
||||
h₁.recOn (fun _ ac₁ _ h₂ => ac₁ y h₂) h₂
|
||||
|
||||
end Acc
|
||||
|
|
@ -58,7 +58,7 @@ class WellFoundedRelation (α : Sort u) where
|
|||
wf : WellFounded rel
|
||||
|
||||
namespace WellFounded
|
||||
def apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
|
||||
theorem apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
|
||||
wf.rec (fun p => p) a
|
||||
|
||||
section
|
||||
|
|
@ -78,7 +78,7 @@ noncomputable def fixF (x : α) (a : Acc r x) : C x := by
|
|||
induction a with
|
||||
| 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
|
||||
theorem 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
|
||||
|
||||
|
|
@ -112,14 +112,14 @@ def emptyWf {α : Sort u} : WellFoundedRelation α where
|
|||
namespace Subrelation
|
||||
variable {α : Sort u} {r q : α → α → Prop}
|
||||
|
||||
def accessible {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a := by
|
||||
theorem accessible {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a := by
|
||||
induction ac with
|
||||
| intro x _ ih =>
|
||||
apply Acc.intro
|
||||
intro y h
|
||||
exact ih y (h₁ h)
|
||||
|
||||
def wf (h₁ : Subrelation q r) (h₂ : WellFounded r) : WellFounded q :=
|
||||
theorem wf (h₁ : Subrelation q r) (h₂ : WellFounded r) : WellFounded q :=
|
||||
⟨fun a => accessible @h₁ (apply h₂ a)⟩
|
||||
end Subrelation
|
||||
|
||||
|
|
@ -136,10 +136,10 @@ private def accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x =
|
|||
subst x
|
||||
apply ih (f y) lt y rfl
|
||||
|
||||
def accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
|
||||
theorem accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
|
||||
accAux f ac a rfl
|
||||
|
||||
def wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
|
||||
theorem wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
|
||||
⟨fun a => accessible f (apply h (f a))⟩
|
||||
end InvImage
|
||||
|
||||
|
|
@ -151,7 +151,7 @@ end InvImage
|
|||
namespace TC
|
||||
variable {α : Sort u} {r : α → α → Prop}
|
||||
|
||||
def accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
|
||||
theorem accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
|
||||
induction ac with
|
||||
| intro x acx ih =>
|
||||
apply Acc.intro x
|
||||
|
|
@ -160,7 +160,7 @@ def accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
|
|||
| base a b rab => exact ih a rab
|
||||
| trans a b c rab _ _ ih₂ => apply Acc.inv (ih₂ acx ih) rab
|
||||
|
||||
def wf (h : WellFounded r) : WellFounded (TC r) :=
|
||||
theorem wf (h : WellFounded r) : WellFounded (TC r) :=
|
||||
⟨fun a => accessible (apply h a)⟩
|
||||
end TC
|
||||
|
||||
|
|
@ -251,7 +251,7 @@ instance [αeqDec : DecidableEq α] {r : α → α → Prop} [rDec : DecidableRe
|
|||
apply isFalse; intro contra; cases contra <;> contradiction
|
||||
|
||||
-- TODO: generalize
|
||||
def right' {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂) :=
|
||||
theorem right' {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂) :=
|
||||
match Nat.eq_or_lt_of_le h₁ with
|
||||
| Or.inl h => h ▸ Prod.Lex.right a₁ h₂
|
||||
| Or.inr h => Prod.Lex.left b₁ _ h
|
||||
|
|
@ -268,7 +268,7 @@ section
|
|||
variable {α : Type u} {β : Type v}
|
||||
variable {ra : α → α → Prop} {rb : β → β → Prop}
|
||||
|
||||
def lexAccessible {a : α} (aca : Acc ra a) (acb : (b : β) → Acc rb b) (b : β) : Acc (Prod.Lex ra rb) (a, b) := by
|
||||
theorem lexAccessible {a : α} (aca : Acc ra a) (acb : (b : β) → Acc rb b) (b : β) : Acc (Prod.Lex ra rb) (a, b) := by
|
||||
induction aca generalizing b with
|
||||
| intro xa _ iha =>
|
||||
induction (acb b) with
|
||||
|
|
@ -347,7 +347,7 @@ variable {α : Sort u} {β : Sort v}
|
|||
def lexNdep (r : α → α → Prop) (s : β → β → Prop) :=
|
||||
Lex r (fun _ => s)
|
||||
|
||||
def lexNdepWf {r : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (lexNdep r s) :=
|
||||
theorem lexNdepWf {r : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (lexNdep r s) :=
|
||||
WellFounded.intro fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha a) (fun _ => hb) b
|
||||
end
|
||||
|
||||
|
|
@ -365,7 +365,7 @@ open WellFounded
|
|||
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
|
||||
theorem 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 a
|
||||
|
|
@ -377,7 +377,7 @@ def revLexAccessible {b} (acb : Acc s b) (aca : (a : α) → Acc r a): (a : α)
|
|||
| left => apply iha; assumption
|
||||
| right => apply ihb; assumption
|
||||
|
||||
def revLex (ha : WellFounded r) (hb : WellFounded s) : WellFounded (RevLex r s) :=
|
||||
theorem revLex (ha : WellFounded r) (hb : WellFounded s) : WellFounded (RevLex r s) :=
|
||||
WellFounded.intro fun ⟨a, b⟩ => revLexAccessible (apply hb b) (WellFounded.apply ha) a
|
||||
end
|
||||
|
||||
|
|
@ -389,7 +389,7 @@ def skipLeft (α : Type u) {β : Type v} (hb : WellFoundedRelation β) : WellFou
|
|||
rel := SkipLeft α hb.rel
|
||||
wf := revLex emptyWf.wf hb.wf
|
||||
|
||||
def mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} (a₁ a₂ : α) (h : s b₁ b₂) : SkipLeft α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ :=
|
||||
theorem mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} (a₁ a₂ : α) (h : s b₁ b₂) : SkipLeft α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ :=
|
||||
RevLex.right _ _ h
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -185,7 +185,7 @@ structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where
|
|||
afterSet : Name → α → AttrM Unit := fun _ _ _ => pure ()
|
||||
afterImport : Array (Array (Name × α)) → ImportM Unit := fun _ => pure ()
|
||||
|
||||
def registerParametricAttribute [Inhabited α] (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
|
||||
def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
|
||||
let ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
|
||||
name := impl.ref
|
||||
mkInitial := pure {}
|
||||
|
|
@ -239,7 +239,7 @@ structure EnumAttributes (α : Type) where
|
|||
ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α)
|
||||
deriving Inhabited
|
||||
|
||||
def registerEnumAttributes [Inhabited α] (attrDescrs : List (Name × String × α))
|
||||
def registerEnumAttributes (attrDescrs : List (Name × String × α))
|
||||
(validate : Name → α → AttrM Unit := fun _ _ => pure ())
|
||||
(applicationTime := AttributeApplicationTime.afterTypeChecking)
|
||||
(ref : Name := by exact decl_name%) : IO (EnumAttributes α) := do
|
||||
|
|
|
|||
|
|
@ -53,7 +53,7 @@ def getMainModuleDoc (env : Environment) : PersistentArray ModuleDoc :=
|
|||
def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array ModuleDoc) :=
|
||||
env.getModuleIdx? moduleName |>.map fun modIdx => moduleDocExt.getModuleEntries env modIdx
|
||||
|
||||
def getDocStringText [Monad m] [MonadError m] [MonadRef m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
|
||||
def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
|
||||
match stx.raw[1] with
|
||||
| Syntax.atom _ val => return val.extract 0 (val.endPos - ⟨2⟩)
|
||||
| _ => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"
|
||||
|
|
|
|||
|
|
@ -39,7 +39,7 @@ def toAttributeKind (attrKindStx : Syntax) : MacroM AttributeKind := do
|
|||
def mkAttrKindGlobal : Syntax :=
|
||||
mkNode ``Lean.Parser.Term.attrKind #[mkNullNode]
|
||||
|
||||
def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadInfoTree m] [MonadLiftT IO m] (attrInstance : Syntax) : m Attribute := do
|
||||
def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (attrInstance : Syntax) : m Attribute := do
|
||||
/- attrInstance := ppGroup $ leading_parser attrKind >> attrParser -/
|
||||
let attrKind ← liftMacroM <| toAttributeKind attrInstance[0]
|
||||
let attr := attrInstance[1]
|
||||
|
|
@ -55,7 +55,7 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa
|
|||
So, we expand them before here before we invoke the attributer handlers implemented using `AttrM`. -/
|
||||
return { kind := attrKind, name := attrName, stx := attr }
|
||||
|
||||
def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m] (attrInstances : Array Syntax) : m (Array Attribute) := do
|
||||
def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (attrInstances : Array Syntax) : m (Array Attribute) := do
|
||||
let mut attrs := #[]
|
||||
for attr in attrInstances do
|
||||
try
|
||||
|
|
@ -65,7 +65,7 @@ def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadM
|
|||
return attrs
|
||||
|
||||
-- leading_parser "@[" >> sepBy1 attrInstance ", " >> "]"
|
||||
def elabDeclAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m] (stx : Syntax) : m (Array Attribute) :=
|
||||
def elabDeclAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (stx : Syntax) : m (Array Attribute) :=
|
||||
elabAttrs stx[1].getSepArgs
|
||||
|
||||
end Lean.Elab
|
||||
|
|
|
|||
|
|
@ -498,7 +498,7 @@ private partial def withSynthesizeImp (k : TermElabM α) (postpone : PostponeBeh
|
|||
Execute `k`, and synthesize pending synthetic metavariables created while executing `k` are solved.
|
||||
If `mayPostpone == false`, then all of them must be synthesized.
|
||||
Remark: even if `mayPostpone == true`, the method still uses `synthesizeUsingDefault` -/
|
||||
@[inline] def withSynthesize [MonadFunctorT TermElabM m] [Monad m] (k : m α) (postpone := PostponeBehavior.no) : m α :=
|
||||
@[inline] def withSynthesize [MonadFunctorT TermElabM m] (k : m α) (postpone := PostponeBehavior.no) : m α :=
|
||||
monadMap (m := TermElabM) (withSynthesizeImp · postpone) k
|
||||
|
||||
private partial def withSynthesizeLightImp (k : TermElabM α) : TermElabM α := do
|
||||
|
|
@ -512,7 +512,7 @@ private partial def withSynthesizeLightImp (k : TermElabM α) : TermElabM α :=
|
|||
modify fun s => { s with pendingMVars := s.pendingMVars ++ pendingMVarsSaved }
|
||||
|
||||
/-- Similar to `withSynthesize`, but uses `postpone := .true`, does not use use `synthesizeUsingDefault` -/
|
||||
@[inline] def withSynthesizeLight [MonadFunctorT TermElabM m] [Monad m] (k : m α) : m α :=
|
||||
@[inline] def withSynthesizeLight [MonadFunctorT TermElabM m] (k : m α) : m α :=
|
||||
monadMap (m := TermElabM) (withSynthesizeLightImp ·) k
|
||||
|
||||
/-- Elaborate `stx`, and make sure all pending synthetic metavariables created while elaborating `stx` are solved. -/
|
||||
|
|
|
|||
|
|
@ -353,7 +353,7 @@ part. `act` is then run on the inner part but with reuse information adjusted as
|
|||
For any tactic that participates in reuse, `withNarrowedTacticReuse` should be applied to the
|
||||
tactic's syntax and `act` should be used to do recursive tactic evaluation of nested parts.
|
||||
-/
|
||||
def withNarrowedTacticReuse [Monad m] [MonadExceptOf Exception m] [MonadWithReaderOf Context m]
|
||||
def withNarrowedTacticReuse [Monad m] [MonadWithReaderOf Context m]
|
||||
[MonadOptions m] [MonadRef m] (split : Syntax → Syntax × Syntax) (act : Syntax → m α)
|
||||
(stx : Syntax) : m α := do
|
||||
let (outer, inner) := split stx
|
||||
|
|
@ -377,7 +377,7 @@ NOTE: child nodes after `argIdx` are not tested (which would almost always disab
|
|||
necessarily shifted by changes at `argIdx`) so it must be ensured that the result of `arg` does not
|
||||
depend on them (i.e. they should not be inspected beforehand).
|
||||
-/
|
||||
def withNarrowedArgTacticReuse [Monad m] [MonadExceptOf Exception m] [MonadWithReaderOf Context m]
|
||||
def withNarrowedArgTacticReuse [Monad m] [MonadWithReaderOf Context m]
|
||||
[MonadOptions m] [MonadRef m] (argIdx : Nat) (act : Syntax → m α) (stx : Syntax) : m α :=
|
||||
withNarrowedTacticReuse (fun stx => (mkNullNode stx.getArgs[:argIdx], stx[argIdx])) act stx
|
||||
|
||||
|
|
@ -387,7 +387,7 @@ to `none`. This should be done for tactic blocks that are run multiple times as
|
|||
reported progress will jump back and forth (and partial reuse for these kinds of tact blocks is
|
||||
similarly questionable).
|
||||
-/
|
||||
def withoutTacticIncrementality [Monad m] [MonadWithReaderOf Context m] [MonadOptions m] [MonadRef m]
|
||||
def withoutTacticIncrementality [Monad m] [MonadWithReaderOf Context m] [MonadOptions m]
|
||||
(cond : Bool) (act : m α) : m α := do
|
||||
let opts ← getOptions
|
||||
withTheReader Term.Context (fun ctx => { ctx with tacSnap? := ctx.tacSnap?.filter fun tacSnap => Id.run do
|
||||
|
|
@ -398,7 +398,7 @@ def withoutTacticIncrementality [Monad m] [MonadWithReaderOf Context m] [MonadOp
|
|||
}) act
|
||||
|
||||
/-- Disables incremental tactic reuse for `act` if `cond` is true. -/
|
||||
def withoutTacticReuse [Monad m] [MonadWithReaderOf Context m] [MonadOptions m] [MonadRef m]
|
||||
def withoutTacticReuse [Monad m] [MonadWithReaderOf Context m] [MonadOptions m]
|
||||
(cond : Bool) (act : m α) : m α := do
|
||||
let opts ← getOptions
|
||||
withTheReader Term.Context (fun ctx => { ctx with tacSnap? := ctx.tacSnap?.map fun tacSnap =>
|
||||
|
|
|
|||
|
|
@ -599,7 +599,7 @@ end TagDeclarationExtension
|
|||
|
||||
def MapDeclarationExtension (α : Type) := SimplePersistentEnvExtension (Name × α) (NameMap α)
|
||||
|
||||
def mkMapDeclarationExtension [Inhabited α] (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α) :=
|
||||
def mkMapDeclarationExtension (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α) :=
|
||||
registerSimplePersistentEnvExtension {
|
||||
name := name,
|
||||
addImportedFn := fun _ => {},
|
||||
|
|
|
|||
|
|
@ -32,8 +32,6 @@ inductive HeadIndex where
|
|||
| forallE
|
||||
deriving Inhabited, BEq, Repr
|
||||
|
||||
namespace HeadIndex
|
||||
|
||||
/-- Hash code for a `HeadIndex` value. -/
|
||||
protected def HeadIndex.hash : HeadIndex → UInt64
|
||||
| fvar fvarId => mixHash 11 <| hash fvarId
|
||||
|
|
@ -47,8 +45,6 @@ protected def HeadIndex.hash : HeadIndex → UInt64
|
|||
|
||||
instance : Hashable HeadIndex := ⟨HeadIndex.hash⟩
|
||||
|
||||
end HeadIndex
|
||||
|
||||
namespace Expr
|
||||
|
||||
/-- Return the number of arguments in the given expression with respect to its `HeadIndex` -/
|
||||
|
|
|
|||
|
|
@ -850,7 +850,7 @@ def foldValues (f : σ → α → σ) (init : σ) (t : DiscrTree α) : σ :=
|
|||
Check for the presence of a value satisfying a predicate.
|
||||
-/
|
||||
@[inline]
|
||||
def containsValueP [BEq α] (t : DiscrTree α) (f : α → Bool) : Bool :=
|
||||
def containsValueP (t : DiscrTree α) (f : α → Bool) : Bool :=
|
||||
t.foldValues (init := false) fun r a => r || f a
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -175,7 +175,7 @@ def ppOrigin [Monad m] [MonadEnv m] [MonadError m] : Origin → m MessageData
|
|||
| .stx _ ref => return ref
|
||||
| .other n => return n
|
||||
|
||||
def ppSimpTheorem [Monad m] [MonadLiftT IO m] [MonadEnv m] [MonadError m] (s : SimpTheorem) : m MessageData := do
|
||||
def ppSimpTheorem [Monad m] [MonadEnv m] [MonadError m] (s : SimpTheorem) : m MessageData := do
|
||||
let perm := if s.perm then ":perm" else ""
|
||||
let name ← ppOrigin s.origin
|
||||
let prio := m!":{s.priority}"
|
||||
|
|
|
|||
|
|
@ -81,7 +81,7 @@ namespace Meta
|
|||
`.const f` is not visited again. Put differently: every `.const f` is visited once, with its
|
||||
arguments if present, on its own otherwise.
|
||||
-/
|
||||
partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] [MonadTrace m] [MonadRef m] [MonadOptions m] [AddMessageContext m]
|
||||
partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
|
||||
(input : Expr)
|
||||
(pre : Expr → m TransformStep := fun _ => return .continue)
|
||||
(post : Expr → m TransformStep := fun e => return .done e)
|
||||
|
|
|
|||
|
|
@ -165,11 +165,11 @@ def getReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) : m Reducibil
|
|||
return getReducibilityStatusCore (← getEnv) declName
|
||||
|
||||
/-- Set the reducibility attribute for the given declaration. -/
|
||||
def setReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit := do
|
||||
def setReducibilityStatus [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit :=
|
||||
modifyEnv fun env => setReducibilityStatusCore env declName s .global .anonymous
|
||||
|
||||
/-- Set the given declaration as `[reducible]` -/
|
||||
def setReducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
|
||||
def setReducibleAttribute [MonadEnv m] (declName : Name) : m Unit :=
|
||||
setReducibilityStatus declName ReducibilityStatus.reducible
|
||||
|
||||
/-- Return `true` if the given declaration has been marked as `[reducible]`. -/
|
||||
|
|
@ -185,7 +185,7 @@ def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
|
|||
| _ => return false
|
||||
|
||||
/-- Set the given declaration as `[irreducible]` -/
|
||||
def setIrreducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
|
||||
def setIrreducibleAttribute [MonadEnv m] (declName : Name) : m Unit :=
|
||||
setReducibilityStatus declName ReducibilityStatus.irreducible
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -307,7 +307,7 @@ def ensureNoOverload [Monad m] [MonadError m] (n : Name) (cs : List Name) : m Na
|
|||
def resolveGlobalConstNoOverloadCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (n : Name) : m Name := do
|
||||
ensureNoOverload n (← resolveGlobalConstCore n)
|
||||
|
||||
def preprocessSyntaxAndResolve [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (stx : Syntax) (k : Name → m (List Name)) : m (List Name) := do
|
||||
def preprocessSyntaxAndResolve [Monad m] [MonadEnv m] [MonadError m] (stx : Syntax) (k : Name → m (List Name)) : m (List Name) := do
|
||||
match stx with
|
||||
| .ident _ _ n pre => do
|
||||
let pre := pre.filterMap fun
|
||||
|
|
|
|||
|
|
@ -16,8 +16,6 @@ if the number of subterms satisfying `p` is a small subset of the set of subterm
|
|||
If `p` holds for most subterms, then it is more efficient to use `forEach f e`.
|
||||
-/
|
||||
|
||||
variable {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m]
|
||||
|
||||
namespace ForEachExprWhere
|
||||
abbrev cacheSize : USize := 8192 - 1
|
||||
|
||||
|
|
@ -37,7 +35,9 @@ unsafe def initCache : State := {
|
|||
checked := {}
|
||||
}
|
||||
|
||||
abbrev ForEachM {ω : Type} (m : Type → Type) [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] := StateRefT' ω State m
|
||||
abbrev ForEachM {ω : Type} (m : Type → Type) [STWorld ω m] := StateRefT' ω State m
|
||||
|
||||
variable {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m]
|
||||
|
||||
unsafe def visited (e : Expr) : ForEachM m Bool := do
|
||||
let s ← get
|
||||
|
|
|
|||
|
|
@ -64,7 +64,7 @@ info: [Meta.debug] (Add.add => (node
|
|||
(* => (node #[5]))
|
||||
(Nat.add => (node (0 => (node (20 => (node #[3]))))))
|
||||
[Meta.debug] #[5, 1]
|
||||
[Meta.debug] Add.add ?m.4906 ?m.4906
|
||||
[Meta.debug] Add.add ?m.4899 ?m.4899
|
||||
[Meta.debug] #[5]
|
||||
[Meta.debug] #[5, 1, 4, 2]
|
||||
[Meta.debug] #[1, 4, 2, 5, 3]
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue