Documentation

Cedar.Thm.SymCC.Tactics

This file contains basic utility tactics. #

source
def Cedar.Thm.tacticSimp_do_let_At_ :
Lean.ParserDescr

This tactic simplifes assumptions of the form do (let x ← expr ...) by performing a cases and simp on expr.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Cedar.Thm.tacticClean_i :
    Lean.ParserDescr
    Equations
    Instances For