Documentation
Aesop
.
Forward
.
Match
Search
return to top
source
Imports
Init
Lean
Aesop.Rule
Aesop.Forward.PremiseIndex
Aesop.Forward.SlotIndex
Aesop.Rule.Forward
Aesop.RuleTac.Descr
Aesop.RuleTac.ElabRuleTerm
Aesop.Script.SpecificTactics
Aesop.Forward.Match.Types
Aesop.RuleTac.Forward.Basic
Batteries.Lean.Meta.UnusedNames
Imported by