Theorems · Definition · logic and foundations
StateTransition.eval
{σ : Type u_1} → (σ → Option σ) → σ → Part σRun a state transition function σ → Option σ "to completion". The return value is the last
state returned before a none result. If the state transition function always returns some,
then the computation diverges, returning Part.none.
- Defined in
- Mathlib.Computability.StateTransition
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by21
Results whose statement or proof uses this declaration.
- StateTransition.mem_evalstatement and proof · cited by 8
- StateTransition.reaches_evalstatement and proof · cited by 4
- StateTransition.tr_evalstatement and proof · cited by 4
- StateTransition.tr_eval_revstatement and proof · cited by 3
- Turing.TM1.evalproof · cited by 3
- Turing.ToPartrec.Code.Okproof · cited by 3
- Turing.TM2.evalproof · cited by 2
- Turing.ToPartrec.code_is_okproof · cited by 2
- Turing.ToPartrec.cont_eval_fixstatement and proof · cited by 2
- StateTransition.evalInductionstatement and proof · cited by 2
- StateTransition.tr_eval_domstatement and proof · cited by 1
- Turing.TM0.evalproof · cited by 1