Documentation

Aesop.Frontend.Tactic

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                aesop <clause>* tries to solve the current goal by applying a set of rules registered with the @[aesop] attribute. See its README for a tutorial and a reference.

                The variant aesop? prints the proof it found as a Try this suggestion.

                Clauses can be used to customise the behaviour of an Aesop call. Available clauses are:

                • (add <phase> <priority> <builder> <rule>) adds a rule. <phase> is unsafe, safe or norm. <priority> is a percentage for unsafe rules and an integer for safe and norm rules. <rule> is the name of a declaration or local hypothesis. <builder> is the rule builder used to turn <rule> into an Aesop rule. Example: (add unsafe 50% apply Or.inl).
                • (erase <rule>) disables a globally registered Aesop rule. Example: (erase Aesop.BuiltinRules.assumption).
                • (rule_sets := [<ruleset>,*]) enables or disables named sets of rules for this Aesop call. Example: (rule_sets := [-builtin, MyRuleSet]).
                • (config { <opt> := <value> }) adjusts Aesop's search options. See Aesop.Options.
                • (simp_config { <opt> := <value> }) adjusts options for Aesop's built-in simp rule. The given options are directly passed to simp. For example, (simp_config := { zeta := false }) makes Aesop use simp (config := { zeta := false }).
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  aesop <clause>* tries to solve the current goal by applying a set of rules registered with the @[aesop] attribute. See its README for a tutorial and a reference.

                  The variant aesop? prints the proof it found as a Try this suggestion.

                  Clauses can be used to customise the behaviour of an Aesop call. Available clauses are:

                  • (add <phase> <priority> <builder> <rule>) adds a rule. <phase> is unsafe, safe or norm. <priority> is a percentage for unsafe rules and an integer for safe and norm rules. <rule> is the name of a declaration or local hypothesis. <builder> is the rule builder used to turn <rule> into an Aesop rule. Example: (add unsafe 50% apply Or.inl).
                  • (erase <rule>) disables a globally registered Aesop rule. Example: (erase Aesop.BuiltinRules.assumption).
                  • (rule_sets := [<ruleset>,*]) enables or disables named sets of rules for this Aesop call. Example: (rule_sets := [-builtin, MyRuleSet]).
                  • (config { <opt> := <value> }) adjusts Aesop's search options. See Aesop.Options.
                  • (simp_config { <opt> := <value> }) adjusts options for Aesop's built-in simp rule. The given options are directly passed to simp. For example, (simp_config := { zeta := false }) makes Aesop use simp (config := { zeta := false }).
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Instances For
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For