Theorems · Inductive type · logic and foundations
Nat.RecursiveIn
Set (ℕ →. ℕ) → (ℕ →. ℕ) → Prop
The type of partial functions recursive in a set of oracles O is the smallest type containing
the constant zero, the successor, left and right projections, each oracle g ∈ O,
and is closed under pairing, composition, primitive recursion, and μ-recursion.
- Defined in
- Mathlib.Computability.RecursiveIn
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by13
Results whose statement or proof uses this declaration.
- RecursiveInproof · cited by 15
- Nat.Partrec.recursiveInstatement and proof · cited by 2
- Nat.RecursiveIn.subststatement and proof · cited by 1
- Nat.RecursiveIn.of_eqstatement and proof · cited by 1
- Nat.RecursiveIn.belowstatement · cited by 1
- RecursiveIn.iff_natstatement and proof · cited by 1
- Nat.RecursiveIn.partrec_of_oraclestatement and proof · cited by 1
- Nat.RecursiveIn.recOnstatement and proof · cited by 0
- Nat.Primrec.recursiveInstatement · cited by 0
- Nat.RecursiveIn.brecOnstatement and proof · cited by 0
- Nat.RecursiveIn.casesOnstatement and proof · cited by 0
- Nat.RecursiveIn.below.casesOnstatement and proof · cited by 0