Theorems · Theorem · logic and foundations
Turing.ToPartrec.stepRet_eval
∀ {k : Turing.ToPartrec.Cont} {v : List ℕ},
StateTransition.eval Turing.ToPartrec.step (Turing.ToPartrec.stepRet k v) = Turing.ToPartrec.Cfg.halt <$> k.eval v- Cited by
- 0 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Partstatement and proof · cited by 325
- PFunproof · cited by 207
- Turing.ToPartrec.Codeproof · cited by 83
- List.headIproof · cited by 42
- Turing.ToPartrec.Contstatement and proof · cited by 33
- Relation.ReflTransGen.singleproof · cited by 26
- Turing.ToPartrec.Code.evalproof · cited by 23
- Turing.ToPartrec.Cfgstatement and proof · cited by 20
- Part.eq_some_iffproof · cited by 17
- StateTransition.evalstatement and proof · cited by 16
- StateTransition.mem_evalproof · cited by 8
- Turing.ToPartrec.stepstatement and proof · cited by 7
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.