Support for collecting function calls that could be used for fun_induction
or fun_cases
.
Used by fun_induction foo
, and the Calls
structure is also used by try?
.
the full calls
- seen : Std.HashSet (Name × Array Expr)
only function name and relevant arguments
Instances For
def
Lean.Meta.FunInd.SeenCalls.push
(e : Expr)
(funIndInfo : FunIndInfo)
(args : Array Expr)
(calls : SeenCalls)
:
Equations
Instances For
Which functions have exactly one candidate application. Used by try?
to determine whether
we can use fun_induction foo
or need fun_induction foo x y z
.
Equations
Instances For
@[reducible, inline]
Equations
Instances For
def
Lean.Meta.FunInd.Collector.saveFunInd
(e : Expr)
(funIndInfo : FunIndInfo)
(args : Array Expr)
:
Equations
Instances For
Equations
Instances For
@[reducible, inline]