def Aesop.forwardHypPrefix : Lean.Name

Prefix of the regular hyps added by forward.

def Aesop.forwardImplDetailHypPrefix : Lean.Name

Prefix of the implDetail hyps added by forward.

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.

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

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

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.

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

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

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

structure Aesop.ForwardHypData : Type

• depths : Std.HashMap Lean.FVarId Nat

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

def Aesop.getForwardHypData : Lean.MetaM ForwardHypData

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.