Documentation

Strata.DL.Lambda.LExprEvalFully

The fixpoint evaluator evalFully #

evalFully runs the fuel-bounded evaluator LExpr.eval at fuel 0, 1, 2, … and returns the first fully reduced result (.value true); it is none when no fuel yields one. Its properties, and the properties of LExpr.eval they rest on, are in LExprEvalFuelProps.

source
@[irreducible]
def Lambda.LExpr.evalFullyAux {TBase : LExprParams} [DecidableEq TBase.IDMeta] [Inhabited TBase.IDMeta] [Traceable EvalProvenance TBase.Metadata] (F : Factory TBase) (env : Env TBase) (e : LExpr TBase.mono) (fuel : Nat) :
Option (LExpr TBase.mono)

Run eval at fuel, fuel + 1, … and return the first fully reduced result (.value true); none when no fuel from fuel on yields one (partial_fixpoint).

@[expose] works around a panic of partial_fixpoint on non-exposed bodies in the current Lean release.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lambda.LExpr.evalFully {TBase : LExprParams} [DecidableEq TBase.IDMeta] [Inhabited TBase.IDMeta] [Traceable EvalProvenance TBase.Metadata] (F : Factory TBase) (env : Env TBase) (e : LExpr TBase.mono) :
    Option (LExpr TBase.mono)

    Fully evaluate an expression: evalFullyAux from fuel 0.

    Equations
    Instances For