Documentation

Aesop.BuiltinRules.Ext

source
def Aesop.BuiltinRules.extCore (goal : Lean.MVarId) :
ScriptM (Option (Array Lean.MVarId))
Equations
    Instances For
      source
      def Aesop.BuiltinRules.ext :
      RuleTac
      Equations
        Instances For