Prefix of the regular hyps added by forward
.
Equations
Instances For
Prefix of the implDetail
hyps added by forward
.
Equations
Instances For
Name of the implDetail
hyp corresponding to the forward hyp
with name
fwdHypName
and depth depth
.
Equations
Instances For
Parse a name generated by forwardImplDetailHypName
, obtaining the
fwdHypName
and depth
.
Equations
Instances For
Check whether the given name was generated by forwardImplDetailHypName
.
We assume that nobody else adds hyps with the forwardImplHypDetailPrefix
prefix.
Equations
Instances For
Equations
Instances For
- depths : Std.HashMap Lean.FVarId Nat
Depths of the hypotheses that have already been added by forward reasoning.
Instances For
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.