HepLean Documentation

Aesop.RuleTac.Preprocess

This RuleTac is applied once to the root goal, before any other rules are tried.

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