Mathlib Map

Theorems · Definition · logic and foundations

Turing.ListBlank.cons

{Γ : Type u_1} → [inst : Inhabited Γ] → Γ → Turing.ListBlank Γ → Turing.ListBlank Γ

We can cons an element onto a ListBlank.

Defined in
Mathlib.Computability.TuringMachine.Tape
Cited by
31 results in Mathlib
Foundations
Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Inhabited
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Turing.Tape.move · cited by 25Tape.moveTuring.ListBlank.head_cons · cited by 18ListBlank.head_consTuring.ListBlank.tail_cons · cited by 17ListBlank.tail_consTuring.ListBlank.cons_head_tail · cited by 13ListBlank.cons_head_tailTuring.TM2to1.addBottom · cited by 12TM2to1.addBottomTuring.Tape.right₀ · cited by 7Tape.right₀Turing.ListBlank.nth_succ · cited by 5ListBlank.nth_succTuring.ListBlank.nth_zero · cited by 4ListBlank.nth_zeroTuring.ListBlank.tail_map · cited by 4ListBlank.tail_mapTuring.ListBlank.head_map · cited by 4ListBlank.head_mapTuring.ListBlank.map_cons · cited by 3ListBlank.map_consTuring.TM1to1.trTape'_move_left · cited by 3TM1to1.trTape'_move_leftTuring.Tape.move_left_mk' · cited by 3Tape.move_left_mk'Turing.Tape.move_right_mk' · cited by 3Tape.move_right_mk'Turing.Tape.write_mk' · cited by 3Tape.write_mk'Turing.ListBlank · cited by 68Turing.ListBlankTuring.ListBlank.mk · cited by 22ListBlank.mkTuring.ListBlank.liftOn · cited by 2ListBlank.liftOnListBlank.consCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by35

Results whose statement or proof uses this declaration.