Theorems · Theorem · logic and foundations
Primrec.snd
∀ {α : Type u_2} {β : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β], Primrec Prod.snd- Defined in
- Mathlib.Computability.Primrec.Basic
- Cited by
- 66 results in Mathlib
- Foundations
- Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PrimcodablePrimcodable
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Primcodablestatement and proof · cited by 325
- Primrecstatement · cited by 141
- Encodable.encodeproof · cited by 118
- Encodable.decodeproof · cited by 77
- Nat.unpairproof · cited by 67
- Nat.pairproof · cited by 62
- Nat.unpair_pairproof · cited by 30
- Nat.Primrec.of_eqproof · cited by 25
- Primcodable.primproof · cited by 17
- Encodable.decode_prod_valproof · cited by 8
- Nat.Primrec.casesOn'proof · cited by 3
Cited by66
Results whose statement or proof uses this declaration.
- Computable.sndproof · cited by 21
- Primrec₂.rightproof · cited by 13
- Primrec.list_getElem?proof · cited by 7
- Primrec.list_lengthproof · cited by 7
- Primrec.list_foldrproof · cited by 6
- Primrec.vector_getproof · cited by 5
- Primrec.list_rangeproof · cited by 4
- Nat.Partrec.ppredproof · cited by 4
- Primrec₂.pairproof · cited by 4
- Nat.Partrec.Code.primrec₂_curryproof · cited by 4
- Partrec.rfindproof · cited by 4
- Primrec.list_appendproof · cited by 4