Documentation
Lean
.
Meta
.
Tactic
.
Grind
.
Arith
.
Model
Search
return to top
source
Imports
Lean.Meta.Basic
Lean.Meta.Tactic.Grind.Types
Lean.Meta.Tactic.Grind.Util
Imported by
Lean
.
Meta
.
Grind
.
Arith
.
Offset
.
mkModel
source
def
Lean
.
Meta
.
Grind
.
Arith
.
Offset
.
mkModel
(goal :
Goal
)
:
MetaM
(
Array
(
Expr
×
Nat
))
Construct a model that statisfies all offset constraints
Equations
One or more equations did not get rendered due to their size.
Instances For