Documentation
Lean
.
Util
.
CollectFVars
Search
Google site search
Lean
.
Util
.
CollectFVars
source
Imports
Init
Lean.Expr
Lean.LocalContext
Imported by
Lean
.
CollectFVars
.
State
Lean
.
CollectFVars
.
instInhabitedState
Lean
.
CollectFVars
.
State
.
add
Lean
.
CollectFVars
.
Visitor
Lean
.
CollectFVars
.
visit
Lean
.
CollectFVars
.
main
Lean
.
collectFVars
source
structure
Lean
.
CollectFVars
.
State
:
Type
visitedExpr :
Lean.ExprSet
fvarSet :
Lean.FVarIdSet
fvarIds :
Array
Lean.FVarId
Instances For
source
instance
Lean
.
CollectFVars
.
instInhabitedState
:
Inhabited
Lean.CollectFVars.State
source
def
Lean
.
CollectFVars
.
State
.
add
(s :
Lean.CollectFVars.State
)
(fvarId :
Lean.FVarId
)
:
Lean.CollectFVars.State
Instances For
source
@[inline, reducible]
abbrev
Lean
.
CollectFVars
.
Visitor
:
Type
Instances For
source
partial def
Lean
.
CollectFVars
.
visit
(e :
Lean.Expr
)
:
Lean.CollectFVars.Visitor
source
partial def
Lean
.
CollectFVars
.
main
:
Lean.Expr
→
Lean.CollectFVars.Visitor
source
def
Lean
.
collectFVars
(s :
Lean.CollectFVars.State
)
(e :
Lean.Expr
)
:
Lean.CollectFVars.State
Instances For