Theorems · Theorem · logic and foundations
Primrec.fin_app
∀ {σ : Type u_3} [inst : Primcodable σ] {n : ℕ}, Primrec₂ id- Defined in
- Mathlib.Computability.Primrec.List
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Primcodable
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Primcodablestatement and proof · cited by 325
- Primrec₂statement · cited by 93
- Primrec.compproof · cited by 80
- Primrec.sndproof · cited by 66
- Primrec.fstproof · cited by 58
- Primrec₂.compproof · cited by 55
- Primrec.of_eqproof · cited by 50
- List.Vector.getproof · cited by 41
- List.Vector.ofFnproof · cited by 16
- List.Vector.get_ofFnproof · cited by 6
- Primrec.vector_getproof · cited by 5
- Primrec.vector_ofFn'proof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- Computable.fin_appproof · cited by 0
- Primrec.fin_curryproof · cited by 0