Documentation
Lean
.
Meta
.
CheckTactic
Search
return to top
source
Imports
Lean.Meta.Basic
Imported by
Lean
.
Meta
.
CheckTactic
.
mkCheckGoalType
Lean
.
Meta
.
CheckTactic
.
matchCheckGoalType
source
def
Lean
.
Meta
.
CheckTactic
.
mkCheckGoalType
(
val
type
:
Expr
)
:
MetaM
Expr
Equations
Instances For
source
def
Lean
.
Meta
.
CheckTactic
.
matchCheckGoalType
(
stx
:
Syntax
)
(
goalType
:
Expr
)
:
MetaM
(
Expr
×
Expr
×
Level
)
Equations
Instances For