def Aesop.forwardHypPrefix : Lean.Name

Prefix of the regular hyps added by forward.

Equations

• Aesop.forwardHypPrefix = `fwd

def Aesop.forwardImplDetailHypPrefix : Lean.Name

Prefix of the implDetail hyps added by forward.

Equations

• Aesop.forwardImplDetailHypPrefix = `__aesop.fwd

def Aesop.forwardImplDetailHypName (fwdHypName : Lean.Name) (depth : Nat) : Lean.Name

Name of the implDetail hyp corresponding to the forward hyp with name fwdHypName and depth depth.

Equations

• Aesop.forwardImplDetailHypName fwdHypName depth = Aesop.forwardImplDetailHypPrefix.num depth ++ fwdHypName

def Aesop.matchForwardImplDetailHypName (n : Lean.Name) : Option (Nat × Lean.Name)

Parse a name generated by forwardImplDetailHypName, obtaining the fwdHypName and depth.

Equations

• One or more equations did not get rendered due to their size.

def Aesop.isForwardImplDetailHypName (n : Lean.Name) : Bool

Check whether the given name was generated by forwardImplDetailHypName. We assume that nobody else adds hyps with the forwardImplHypDetailPrefix prefix.

Equations

• Aesop.isForwardImplDetailHypName n = `__aesop.fwd.isPrefixOf n

def Aesop.isForwardImplDetailHyp (ldecl : Lean.LocalDecl) : Bool

Equations

• Aesop.isForwardImplDetailHyp ldecl = (ldecl.isImplementationDetail && Aesop.isForwardImplDetailHypName ldecl.userName)

def Aesop.getForwardImplDetailHyps : Lean.MetaM (Array Lean.LocalDecl)

Equations

• One or more equations did not get rendered due to their size.

def Aesop.clearForwardImplDetailHyps (goal : Lean.MVarId) : Lean.MetaM Lean.MVarId

Equations

• Aesop.clearForwardImplDetailHyps goal = goal.withContext do let hyps ← Aesop.getForwardImplDetailHyps goal.tryClearMany (Array.map (fun (x : Lean.LocalDecl) => x.fvarId) hyps)

structure Aesop.ForwardHypData : Type

• types : Array Lean.Expr

  Types of the hypotheses that have already been added by forward reasoning.

• depths : Std.HashMap Lean.FVarId Nat

  Depths of the hypotheses that have already been added by forward reasoning.

def Aesop.getForwardHypData : Lean.MetaM Aesop.ForwardHypData

Equations

• One or more equations did not get rendered due to their size.

def Aesop.ForwardHypData.containsTypeUpToIds (data : Aesop.ForwardHypData) (type : Lean.Expr) : Lean.MetaM Bool

Equations

• data.containsTypeUpToIds type = Array.anyM (fun (knownType : Lean.Expr) => Aesop.exprsEqualUpToIds' type knownType true) data.types

def Aesop.hideForwardImplDetailHyps (goal : Lean.MVarId) : Lean.MetaM Lean.MVarId

Mark hypotheses that, according to their name, are forward implementation detail hypotheses, as implementation details. This is a hack that works around the fact that certain tactics (particularly anything based on the revert-intro pattern) can turn implementation detail hyps into regular hyps.

Equations

• One or more equations did not get rendered due to their size.