Theorems · Definition · logic and foundations
Turing.ListBlank.nth
{Γ : Type u_1} → [inst : Inhabited Γ] → Turing.ListBlank Γ → ℕ → ΓThe n-th element of a ListBlank is well defined for all n : ℕ, unlike in a List.
- Defined in
- Mathlib.Computability.TuringMachine.Tape
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Inhabited
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.
- Turing.ListBlankstatement and proof · cited by 68
- List.getIproof · cited by 17
- Turing.ListBlank.liftOnproof · cited by 2
Cited by18
Results whose statement or proof uses this declaration.
- Turing.Tape.nthproof · cited by 8
- Turing.ListBlank.nth_succstatement and proof · cited by 5
- Turing.Tape.mk'_nth_natstatement and proof · cited by 4
- Turing.ListBlank.nth_mapstatement · cited by 4
- Turing.ListBlank.nth_zerostatement and proof · cited by 4
- Turing.ListBlank.nth_mkstatement · cited by 3
- Turing.TM2to1.addBottom_nth_sndstatement and proof · cited by 3
- Turing.TM2to1.stk_nth_valstatement and proof · cited by 3
- Turing.ListBlank.extstatement and proof · cited by 3
- Turing.TM2to1.addBottom_nth_succ_fststatement and proof · cited by 2
- Turing.TM2to1.trCfg_initproof · cited by 2
- Turing.proj_map_nthstatement and proof · cited by 2