Documentation

Lean.Meta.Tactic.Grind.Core

Returns true if e is True, False, or a literal value. See LitValues for supported literals.

Equations

Creates an ENode for e if one does not already exist. This method assumes e has been hashconsed.

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

Returns the root element in the equivalence class of e.

Equations

Returns the next element in the equivalence class of e.

Equations