Aesop SimpleRuleTac vs SingleRuleTac

Stream: metaprogramming / tactics

[Geoffrey Irving]

The Aesop README mentions SimpleRuleTac, but I can’t find that type in the code. Is it supposed to be SingleRuleTac? There are some suspicious comments:

-- Precondition: `decl` has type `SimpleRuleTac`.
unsafe def singleRuleTacImpl (decl : Name) : RuleTac :=
  SingleRuleTac.toRuleTac λ input => do
    let tac ← evalConst SingleRuleTac decl
    tac input

[Geoffrey Irving]

Cc @Jannis Limperg

[Geoffrey Irving]

(deleted)

[Jannis Limperg]

Very likely the README is outdated. Will fix once I'm at my laptop again.