TorchLean API

Docs HomeGuideExamplesGraphs

Lean.Meta.CheckTactic

source
def Lean.Meta.CheckTactic.mkCheckGoalType (val type : Expr) :
MetaM Expr
Instances For
    source
    def Lean.Meta.CheckTactic.matchCheckGoalType (stx : Syntax) (goalType : Expr) :
    MetaM (Expr × Expr × Level)
    Instances For