Documentation

Cedar.Thm.SymCC.Tactics

This file contains basic utility tactics specific to symbolic compilation. General-purpose tactics live in Cedar.Thm.Tactics. #

source
def Cedar.Thm.tacticClean_i :
Lean.ParserDescr
Equations
Instances For