Set the kind of a LocalDecl
.
Instances For
Set the kind of the given fvar.
Instances For
Sort the given FVarId
s by the order in which they appear in lctx
. If any of
the FVarId
s do not appear in lctx
, the result is unspecified.
Instances For
Sort the given FVarId
s by the order in which they appear in the current local
context. If any of the FVarId
s do not appear in the current local context, the
result is unspecified.
Instances For
Get the MetavarDecl
of mvarId
. If mvarId
is not a declared metavariable
in the given MetavarContext
, throw an error.
Instances For
Declare a metavariable. You must make sure that the metavariable is not already declared.
Instances For
Check whether a metavariable is assigned or delayed-assigned. A delayed-assigned metavariable is already 'solved' but the solution cannot be substituted yet because we have to wait for some other metavariables to be assigned first. So in most situations you want to treat a delayed-assigned metavariable as assigned.
Instances For
Check whether a metavariable is declared in the given MetavarContext
.
Instances For
Add a delayed assignment for the given metavariable. You must make sure that the metavariable is not already assigned or delayed-assigned.
Instances For
Erase any assignment or delayed assignment of the given metavariable.
Instances For
Modify the declaration of a metavariable. If the metavariable is not declared,
the MetavarContext
is returned unchanged.
You must ensure that the modification is legal. In particular, expressions may only be replaced with defeq expressions.
Instances For
Modify the local context of a metavariable. If the metavariable is not declared,
the MetavarContext
is returned unchanged.
You must ensure that the modification is legal. In particular, expressions may only be replaced with defeq expressions.
Instances For
Set the kind of an fvar. If the given metavariable is not declared or the
given fvar doesn't exist in its context, the MetavarContext
is returned
unchanged.
Instances For
Set the BinderInfo
of an fvar. If the given metavariable is not declared or
the given fvar doesn't exist in its context, the MetavarContext
is returned
unchanged.
Instances For
Obtain all unassigned metavariables from the given MetavarContext
. If
includeDelayed
is true
, delayed-assigned metavariables are considered
unassigned.
Instances For
Check whether a metavariable is assigned or delayed-assigned. A delayed-assigned metavariable is already 'solved' but the solution cannot be substituted yet because we have to wait for some other metavariables to be assigned first. So in most situations you want to treat a delayed-assigned metavariable as assigned.
Instances For
Check whether a metavariable is declared.
Instances For
Add a delayed assignment for the given metavariable. You must make sure that the metavariable is not already assigned or delayed-assigned.
Instances For
Erase any assignment or delayed assignment of the given metavariable.
Instances For
Modify the declaration of a metavariable. If the metavariable is not declared, nothing happens.
You must ensure that the modification is legal. In particular, expressions may only be replaced with defeq expressions.
Instances For
Modify the local context of a metavariable. If the metavariable is not declared, nothing happens.
You must ensure that the modification is legal. In particular, expressions may only be replaced with defeq expressions.
Instances For
Set the kind of an fvar. If the given metavariable is not declared or the given fvar doesn't exist in its context, nothing happens.
Instances For
Set the BinderInfo
of an fvar. If the given metavariable is not declared or
the given fvar doesn't exist in its context, nothing happens.
Instances For
Collect the metavariables which mvarId
depends on. These are the metavariables
which appear in the type and local context of mvarId
, as well as the
metavariables which those metavariables depend on, etc.
Instances For
Auxiliary definition for getMVarDependencies
.
Auxiliary definition for getMVarDependencies
.
Obtain all unassigned metavariables. If includeDelayed
is true
,
delayed-assigned metavariables are considered unassigned.
Instances For
Run a computation with hygiene turned off.
Instances For
A variant of mkFreshId
which generates names with a particular prefix. The
generated names are unique and have the form
where N
is a
natural number. They are not suitable as user-facing names.
Instances For
Implementation of repeat'
and repeat1'
.
repeat'Core f
runs f
on all of the goals to produce a new list of goals,
then runs f
again on all of those goals, and repeats until f
fails on all remaining goals,
or until maxIters
total calls to f
have occurred.
Returns a boolean indicating whether f
succeeded at least once, and
all the remaining goals (i.e. those on which f
failed).
Instances For
Auxiliary for repeat'Core
. repeat'Core.go f maxIters progress gs stk acc
evaluates to
essentially acc.toList ++ repeat' f (gs::stk).join maxIters
: that is, acc
are goals we will
not revisit, and (gs::stk).join
is the accumulated todo list of subgoals.
Equations
- One or more equations did not get rendered due to their size.
- Lean.Meta.repeat'Core.go f x x [] [] x = pure (x, x)
- Lean.Meta.repeat'Core.go f x x [] (gs :: stk) x = Lean.Meta.repeat'Core.go f x x gs stk x
Instances For
repeat' f
runs f
on all of the goals to produce a new list of goals,
then runs f
again on all of those goals, and repeats until f
fails on all remaining goals,
or until maxIters
total calls to f
have occurred.
Always succeeds (returning the original goals if f
fails on all of them).
Instances For
repeat1' f
runs f
on all of the goals to produce a new list of goals,
then runs f
again on all of those goals, and repeats until f
fails on all remaining goals,
or until maxIters
total calls to f
have occurred.
Fails if f
does not succeed at least once.
Instances For
saturate1 goal tac
runs tac
on goal
, then on the resulting goals, etc.,
until tac
does not apply to any goal any more (i.e. it returns none
). The
order of applications is depth-first, so if tac
generates goals [g₁, g₂, ⋯]
,
we apply tac
to g₁
and recursively to all its subgoals before visiting g₂
.
If tac
does not apply to goal
, saturate1
returns none
. Otherwise it
returns the generated subgoals to which tac
did not apply. saturate1
respects the MonadRecDepth
recursion limit.
Instances For
Auxiliary definition for saturate1
.