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?
.
Equations
Equations
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
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
Equations
Instances For
def
Lean.Meta.FunInd.Collector.saveFunInd
(e : Expr)
(funIndInfo : FunIndInfo)
(args : Array Expr)
:
Equations
- Lean.Meta.FunInd.Collector.saveFunInd e funIndInfo args = do let __do_lift ← get let __do_lift ← liftM (Lean.Meta.FunInd.SeenCalls.push e funIndInfo args __do_lift) set __do_lift
Instances For
Equations
- Lean.Meta.FunInd.Collector.visitApp e funIndInfo args = Lean.Meta.FunInd.Collector.saveFunInd e funIndInfo args
Instances For
@[reducible, inline]
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.FunInd.collect needle mvarId = Lean.Meta.FunInd.collect.unsafe_impl_3 needle mvarId