Equations
- Aesop.time x = do let start ← liftM IO.monoNanosNow let a ← x let stop ← liftM IO.monoNanosNow pure (a, { nanos := stop - start })
Instances For
Equations
- Aesop.time' x = do let start ← liftM IO.monoNanosNow x let stop ← liftM IO.monoNanosNow pure { nanos := stop - start }
Instances For
Equations
- Aesop.PersistentHashSet.toList s = Lean.PersistentHashSet.fold (fun (as : List α) (a : α) => a :: as) [] s
Instances For
Equations
- Aesop.PersistentHashSet.toArray s = Lean.PersistentHashSet.fold (fun (as : Array α) (a : α) => as.push a) #[] s
Instances For
Equations
- Aesop.PersistentHashSet.toHashSet s = Lean.PersistentHashSet.fold (fun (result : Std.HashSet α) (a : α) => result.insert a) ∅ s
Instances For
Equations
- Aesop.PersistentHashSet.filter p s = Lean.PersistentHashSet.fold (fun (s : Lean.PHashSet α) (a : α) => if p a = true then s else Lean.PersistentHashSet.erase s a) s s
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Aesop.isEmptyTrie (Lean.Meta.DiscrTree.Trie.node vs children) = (vs.isEmpty && children.isEmpty)
Instances For
Remove elements for which p
returns false
from the given DiscrTree
.
The removed elements are monadically folded over using f
and init
, so f
is called once for each removed element and the final state of type σ
is
returned.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Remove elements for which p
returns false
from the given DiscrTree
.
The removed elements are folded over using f
and init
, so f
is called
once for each removed element and the final state of type σ
is returned.
Equations
- Aesop.filterDiscrTree p f init t = (Aesop.filterDiscrTreeM (fun (a : α) => pure { down := p a }) (fun (s : σ) (a : α) => pure (f s a)) init t).run
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Aesop.SimpTheorems.addSimpEntry s (Lean.Meta.SimpEntry.toUnfoldThms n thms) = s.registerDeclToUnfoldThms n thms
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Aesop.SimpTheorems.foldSimpEntriesM.processTheorem f thms s thm = if Lean.PersistentHashSet.contains thms.erased thm.origin = true then pure s else f s (Lean.Meta.SimpEntry.thm thm)
Instances For
Equations
- Aesop.SimpTheorems.foldSimpEntries f init thms = (Aesop.SimpTheorems.foldSimpEntriesM f init thms).run
Instances For
Equations
- Aesop.SimpTheorems.simpEntries thms = Aesop.SimpTheorems.foldSimpEntries (fun (s : Array Lean.Meta.SimpEntry) (thm : Lean.Meta.SimpEntry) => s.push thm) #[] thms
Instances For
Equations
- Aesop.SimpTheorems.containsDecl thms decl = (thms.isLemma (Lean.Meta.Origin.decl decl) || thms.isDeclToUnfold decl || Lean.PersistentHashMap.contains thms.toUnfoldThms decl)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Aesop.forEachExprInLDecl' ldecl g = (Aesop.forEachExprInLDeclCore ldecl g).run
Instances For
Equations
- Aesop.forEachExprInLDecl ldecl g = (Aesop.forEachExprInLDeclCore ldecl fun (e : Lean.Expr) => do g e pure true).run
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Aesop.forEachExprInLCtx' mvarId g = mvarId.withContext do let __do_lift ← liftM mvarId.getDecl (Aesop.forEachExprInLCtxCore __do_lift.lctx g).run
Instances For
Equations
- Aesop.forEachExprInLCtx mvarId g = Aesop.forEachExprInLCtx' mvarId fun (e : Lean.Expr) => do g e pure true
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Aesop.forEachExprInGoal' mvarId g = (Aesop.forEachExprInGoalCore mvarId g).run
Instances For
Equations
- Aesop.forEachExprInGoal mvarId g = Aesop.forEachExprInGoal' mvarId fun (e : Lean.Expr) => do g e pure true
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
- Aesop.runTacticSyntaxAsMetaM stx goals = do let __do_lift ← Aesop.runTacticMAsMetaM (Lean.Elab.Tactic.evalTactic stx) goals pure __do_lift.snd
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Aesop.updateSimpEntryPriority priority (Lean.Meta.SimpEntry.toUnfoldThms a a_1) = Lean.Meta.SimpEntry.toUnfoldThms a a_1
- Aesop.updateSimpEntryPriority priority (Lean.Meta.SimpEntry.toUnfold a) = Lean.Meta.SimpEntry.toUnfold a
Instances For
Equations
- Aesop.hasSorry e = do let __do_lift ← Lean.getMCtx pure (Aesop.hasSorry.go __do_lift e)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
If the input expression e
reduces to f x₁ ... xₙ
via repeated whnf
, this
function returns f
and [x₁, ⋯, xₙ]
. Otherwise it returns e
(unchanged, not
in WHNF!) and []
.
Equations
Instances For
Partition an array of structures containing MVarId
s into 'goals' and
'proper mvars'. An MVarId
from the input array goals
is classified as a
proper mvar if any of the MVarId
s depend on it, and as a goal otherwise.
Additionally, for each goal, we report the set of mvars that the goal depends
on.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Aesop.runTacticCapturingPostState t preState preGoals = Aesop.runTacticMCapturingPostState (Lean.Elab.Tactic.evalTactic t.raw) preState preGoals
Instances For
Equations
- Aesop.runTacticSeqCapturingPostState t preState preGoals = Aesop.runTacticMCapturingPostState (Lean.Elab.Tactic.evalTactic t.raw) preState preGoals
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Aesop.withTransparencySeqSyntax Lean.Meta.TransparencyMode.default k = (pure k).run
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Aesop.withAllTransparencySeqSyntax md k = k
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Aesop.withTransparencySyntax Lean.Meta.TransparencyMode.default k = (pure k).run
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Aesop.withAllTransparencySyntax md k = k
Instances For
Register a "Try this" suggestion for a tactic sequence.
It works when the tactic to replace appears on its own line:
by
aesop?
It doesn't work (i.e., the suggestion will appear but in the wrong place) when the tactic to replace is preceded by other text on the same line:
have x := by aesop?
The Try this:
suggestion in the infoview is not correctly formatted, but
there's nothing we can do about this at the moment.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Note: the returned local context contains invalid LocalDecl
s.
Equations
- Aesop.getUnusedNames lctx suggestions = Aesop.getUnusedNames.go suggestions 0 (Array.mkEmpty suggestions.size) lctx
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Aesop.getUnusedNames.dummyLDecl name = Lean.LocalDecl.cdecl 0 { name := `_ } name (Lean.Expr.sort Lean.levelZero) Lean.BinderInfo.default Lean.LocalDeclKind.default
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Aesop.withExceptionPrefix pre = Aesop.withExceptionTransform fun (msg : Lean.MessageData) => pre ++ msg
Instances For
Equations
- Aesop.withPPAnalyze x = Lean.withOptions (fun (x : Lean.Options) => (Lean.KVMap.setBool x `pp.analyze true).setBool `pp.proofs true) x
Instances For
Equations
- Aesop.instMonadCacheStateRefT'_aesop = { findCached? := fun (a : α) => liftM (Lean.MonadCache.findCached? a), cache := fun (a : α) (b : β) => liftM (Lean.MonadCache.cache a b) }
Instances For
A generalized variant of Meta.SavedState.runMetaM
Equations
- Aesop.runInMetaState s x = do let initialState ← have this := Lean.saveState; liftM this tryFinally (do liftM s.restore x) (liftM initialState.restore)
Instances For
Equations
Instances For
Equations
- Aesop.compareArraySizeThenLex cmp xs ys = (compare xs.size ys.size).then (Aesop.compareArrayLex cmp xs ys)