The primitive recursive functions #
The primitive recursive functions are the least collection of functions
ℕ → ℕ which are closed under projections (using the pair
pairing function), composition, zero, successor, and primitive recursion
(i.e. Nat.rec where the motive is C n := ℕ).
We can extend this definition to a large class of basic types by
using canonical encodings of types as natural numbers (Gödel numbering),
which we implement through the type class Encodable. (More precisely,
we need that the composition of encode with decode yields a
primitive recursive function, so we have the Primcodable type class
for this.)
In the above, the pairing function is primitive recursive by definition.
This deviates from the textbook definition of primitive recursive functions,
which instead work with n-ary functions. We formalize the textbook
definition in Nat.Primrec'. Nat.Primrec'.prim_iff then proves it is
equivalent to our chosen formulation. For more discussion of this and
other design choices in this formalization, see [Car19].
Main definitions #
Nat.Primrec f:fis primitive recursive, for functionsf : ℕ → ℕPrimrec f:fis primitive recursive, for functions betweenPrimcodabletypesPrimcodable α: well-behaved encoding ofαintoℕ, i.e. one such that roundtripping through the encoding functions adds no computational power
References #
@[reducible]
Calls the given function on a pair of entries n, encoded via the pairing function.
Equations
- Nat.unpaired f n = f (Nat.unpair n).1 (Nat.unpair n).2
Instances For
The primitive recursive functions ℕ → ℕ.
- zero : Nat.Primrec fun (x : ℕ) => 0
- succ : Nat.Primrec succ
- left : Nat.Primrec fun (n : ℕ) => (unpair n).1
- right : Nat.Primrec fun (n : ℕ) => (unpair n).2
- pair {f g : ℕ → ℕ} : Nat.Primrec f → Nat.Primrec g → Nat.Primrec fun (n : ℕ) => Nat.pair (f n) (g n)
- comp {f g : ℕ → ℕ} : Nat.Primrec f → Nat.Primrec g → Nat.Primrec fun (n : ℕ) => f (g n)
- prec {f g : ℕ → ℕ} : Nat.Primrec f → Nat.Primrec g → Nat.Primrec (unpaired fun (z n : ℕ) => Nat.rec (f z) (fun (y IH : ℕ) => g (Nat.pair z (Nat.pair y IH))) n)
Instances For
theorem
Nat.Primrec.prec1
{f : ℕ → ℕ}
(m : ℕ)
(hf : Nat.Primrec f)
:
Nat.Primrec fun (n : ℕ) => Nat.rec m (fun (y IH : ℕ) => f (Nat.pair y IH)) n
theorem
Nat.Primrec.casesOn1
{f : ℕ → ℕ}
(m : ℕ)
(hf : Nat.Primrec f)
:
Nat.Primrec fun (x : ℕ) => Nat.casesOn x m f
theorem
Nat.Primrec.casesOn'
{f g : ℕ → ℕ}
(hf : Nat.Primrec f)
(hg : Nat.Primrec g)
:
Nat.Primrec (unpaired fun (z n : ℕ) => Nat.casesOn n (f z) fun (y : ℕ) => g (Nat.pair z y))
theorem
Nat.Primrec.swap'
{f : ℕ → ℕ → ℕ}
(hf : Nat.Primrec (unpaired f))
:
Nat.Primrec (unpaired (Function.swap f))
A Primcodable type is, essentially, an Encodable type for which
the encode/decode functions are primitive recursive.
However, such a definition is circular.
Instead, we ask that the composition of decode : ℕ → Option α with
encode : Option α → ℕ is primitive recursive. Said composition is
the identity function, restricted to the image of encode.
Thus, in a way, the added requirement ensures that no predicates
can be smuggled in through a cunning choice of the subset of ℕ into
which the type is encoded.
- prim : Nat.Primrec fun (n : ℕ) => Encodable.encode (Encodable.decode n)
Instances
@[instance 10]
Equations
- Primcodable.ofDenumerable α = { toEncodable := inst✝.toEncodable, prim := ⋯ }
Builds a Primcodable instance from an equivalence to a Primcodable type.
Equations
- Primcodable.ofEquiv α e = { toEncodable := Encodable.ofEquiv α e, prim := ⋯ }
Instances For
Equations
- Primcodable.empty = { toEncodable := IsEmpty.toEncodable, prim := Nat.Primrec.zero }
Equations
- Primcodable.unit = { toEncodable := PUnit.encodable, prim := Primcodable.unit._proof_2 }
Equations
- Primcodable.option = { toEncodable := Option.encodable, prim := ⋯ }
Equations
- Primcodable.bool = { toEncodable := Bool.encodable, prim := Primcodable.bool._proof_1 }
Primrec f means f is primitive recursive (after
encoding its input and output as natural numbers).
Equations
- Primrec f = Nat.Primrec fun (n : ℕ) => Encodable.encode (Option.map f (Encodable.decode n))
Instances For
theorem
Primrec.dom_denumerable
{α : Type u_4}
{β : Type u_5}
[Denumerable α]
[Primcodable β]
{f : α → β}
:
theorem
Primrec.encdec
{α : Type u_1}
[Primcodable α]
:
Primrec fun (n : ℕ) => Encodable.encode (Encodable.decode n)
theorem
Primrec.of_eq
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{f g : α → σ}
(hf : Primrec f)
(H : ∀ (n : α), f n = g n)
:
Primrec g
theorem
Primrec.const
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
(x : σ)
:
Primrec fun (x_1 : α) => x
theorem
Primrec.comp
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : β → σ}
{g : α → β}
(hf : Primrec f)
(hg : Primrec g)
:
Primrec fun (a : α) => f (g a)
theorem
Primrec.encode_iff
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{f : α → σ}
:
theorem
Primrec.ofNat_iff
{α : Type u_4}
{β : Type u_5}
[Denumerable α]
[Primcodable β]
{f : α → β}
:
theorem
Primrec.option_some_iff
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{f : α → σ}
:
theorem
Primrec.of_equiv_iff
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{β : Type u_4}
(e : β ≃ α)
{f : σ → β}
:
theorem
Primrec.of_equiv_symm_iff
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{β : Type u_4}
(e : β ≃ α)
{f : σ → α}
:
instance
Primcodable.prod
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
:
Primcodable (α × β)
Equations
- Primcodable.prod = { toEncodable := Encodable.Prod.encodable, prim := ⋯ }
theorem
Primrec.pair
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Primcodable α]
[Primcodable β]
[Primcodable γ]
{f : α → β}
{g : α → γ}
(hf : Primrec f)
(hg : Primrec g)
:
def
Primrec₂
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
(f : α → β → σ)
:
Primrec₂ f means f is a binary primitive recursive function.
This is technically unnecessary since we can always curry all
the arguments together, but there are enough natural two-arg
functions that it is convenient to express this directly.
Instances For
PrimrecPred p means p : α → Prop is a
primitive recursive predicate, which is to say that
decide ∘ p : α → Bool is primitive recursive.
Equations
- PrimrecPred p = ∃ (x : DecidablePred p), Primrec fun (a : α) => decide (p a)
Instances For
PrimrecRel p means p : α → β → Prop is a
primitive recursive relation, which is to say that
decide ∘ p : α → β → Bool is primitive recursive.
Equations
- PrimrecRel s = PrimrecPred fun (p : α × β) => s p.1 p.2
Instances For
theorem
Primrec₂.mk
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → β → σ}
(hf : Primrec fun (p : α × β) => f p.1 p.2)
:
Primrec₂ f
theorem
Primrec₂.of_eq
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f g : α → β → σ}
(hg : Primrec₂ f)
(H : ∀ (a : α) (b : β), f a b = g a b)
:
Primrec₂ g
theorem
Primrec₂.const
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
(x : σ)
:
Primrec₂ fun (x_1 : α) (x_2 : β) => x
theorem
Primrec₂.left
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
:
Primrec₂ fun (a : α) (x : β) => a
theorem
Primrec₂.right
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
:
Primrec₂ fun (x : α) (b : β) => b
theorem
Primrec₂.encode_iff
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → β → σ}
:
theorem
Primrec₂.option_some_iff
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → β → σ}
:
theorem
Primrec₂.ofNat_iff
{α : Type u_4}
{β : Type u_5}
{σ : Type u_6}
[Denumerable α]
[Denumerable β]
[Primcodable σ]
{f : α → β → σ}
:
theorem
Primrec₂.uncurry
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → β → σ}
:
theorem
Primrec₂.curry
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α × β → σ}
:
theorem
Primrec.comp₂
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{σ : Type u_5}
[Primcodable α]
[Primcodable β]
[Primcodable γ]
[Primcodable σ]
{f : γ → σ}
{g : α → β → γ}
(hf : Primrec f)
(hg : Primrec₂ g)
:
Primrec₂ fun (a : α) (b : β) => f (g a b)
theorem
Primrec₂.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{σ : Type u_5}
[Primcodable α]
[Primcodable β]
[Primcodable γ]
[Primcodable σ]
{f : β → γ → σ}
{g : α → β}
{h : α → γ}
(hf : Primrec₂ f)
(hg : Primrec g)
(hh : Primrec h)
:
Primrec fun (a : α) => f (g a) (h a)
theorem
Primrec₂.comp₂
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{σ : Type u_5}
[Primcodable α]
[Primcodable β]
[Primcodable γ]
[Primcodable δ]
[Primcodable σ]
{f : γ → δ → σ}
{g : α → β → γ}
{h : α → β → δ}
(hf : Primrec₂ f)
(hg : Primrec₂ g)
(hh : Primrec₂ h)
:
Primrec₂ fun (a : α) (b : β) => f (g a b) (h a b)
theorem
PrimrecPred.decide
{α : Type u_1}
[Primcodable α]
{p : α → Prop}
[DecidablePred p]
(hp : PrimrecPred p)
:
theorem
Primrec.primrecPred
{α : Type u_1}
[Primcodable α]
{p : α → Prop}
[DecidablePred p]
(hp : Primrec fun (a : α) => decide (p a))
:
theorem
primrecPred_iff_primrec_decide
{α : Type u_1}
[Primcodable α]
{p : α → Prop}
[DecidablePred p]
:
theorem
PrimrecPred.comp
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{p : β → Prop}
{f : α → β}
(hp : PrimrecPred p)
(hf : Primrec f)
:
PrimrecPred fun (a : α) => p (f a)
theorem
PrimrecRel.decide
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{R : α → β → Prop}
[DecidableRel R]
(hR : PrimrecRel R)
:
theorem
Primrec₂.primrecRel
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{R : α → β → Prop}
[DecidableRel R]
(hp : Primrec₂ fun (a : α) (b : β) => decide (R a b))
:
theorem
primrecRel_iff_primrec_decide
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{R : α → β → Prop}
[DecidableRel R]
:
theorem
PrimrecRel.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable γ]
{R : β → γ → Prop}
{f : α → β}
{g : α → γ}
(hR : PrimrecRel R)
(hf : Primrec f)
(hg : Primrec g)
:
PrimrecPred fun (a : α) => R (f a) (g a)
theorem
PrimrecRel.comp₂
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[Primcodable α]
[Primcodable β]
[Primcodable γ]
[Primcodable δ]
{R : γ → δ → Prop}
{f : α → β → γ}
{g : α → β → δ}
:
PrimrecRel R → Primrec₂ f → Primrec₂ g → PrimrecRel fun (a : α) (b : β) => R (f a b) (g a b)
theorem
PrimrecPred.of_eq
{α : Type u_1}
[Primcodable α]
{p q : α → Prop}
(hp : PrimrecPred p)
(H : ∀ (a : α), p a ↔ q a)
:
theorem
PrimrecRel.of_eq
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{r s : α → β → Prop}
(hr : PrimrecRel r)
(H : ∀ (a : α) (b : β), r a b ↔ s a b)
:
theorem
Primrec₂.swap
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → β → σ}
(h : Primrec₂ f)
:
theorem
PrimrecRel.swap
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{r : α → β → Prop}
(h : PrimrecRel r)
:
theorem
Primrec₂.nat_iff
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → β → σ}
:
Primrec₂ f ↔ Nat.Primrec
(Nat.unpaired fun (m n : ℕ) =>
Encodable.encode ((Encodable.decode m).bind fun (a : α) => Option.map (f a) (Encodable.decode n)))
theorem
Primrec₂.nat_iff'
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → β → σ}
:
Primrec₂ f ↔ Primrec₂ fun (m n : ℕ) => (Encodable.decode m).bind fun (a : α) => Option.map (f a) (Encodable.decode n)
theorem
Primrec.to₂
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α × β → σ}
(hf : Primrec f)
:
theorem
PrimrecPred.primrecRel
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{p : α × β → Prop}
(hp : PrimrecPred p)
:
PrimrecRel fun (a : α) (b : β) => p (a, b)
theorem
Primrec.nat_casesOn'
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{f : α → β}
{g : α → ℕ → β}
(hf : Primrec f)
(hg : Primrec₂ g)
:
Primrec₂ fun (a : α) (n : ℕ) => Nat.casesOn n (f a) (g a)
theorem
Primrec.nat_casesOn
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{f : α → ℕ}
{g : α → β}
{h : α → ℕ → β}
(hf : Primrec f)
(hg : Primrec g)
(hh : Primrec₂ h)
:
Primrec fun (a : α) => Nat.casesOn (f a) (g a) (h a)
theorem
Primrec.nat_casesOn₁
{α : Type u_1}
[Primcodable α]
{f : ℕ → α}
(a : α)
(hf : Primrec f)
:
Primrec fun (n : ℕ) => Nat.casesOn n a f
theorem
Primrec.nat_iterate
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{f : α → ℕ}
{g : α → β}
{h : α → β → β}
(hf : Primrec f)
(hg : Primrec g)
(hh : Primrec₂ h)
:
theorem
Primrec.option_casesOn
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{o : α → Option β}
{f : α → σ}
{g : α → β → σ}
(ho : Primrec o)
(hf : Primrec f)
(hg : Primrec₂ g)
:
Primrec fun (a : α) => Option.casesOn (o a) (f a) (g a)
theorem
Primrec.option_bind
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → Option β}
{g : α → β → Option σ}
(hf : Primrec f)
(hg : Primrec₂ g)
:
theorem
Primrec.option_bind₁
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{f : α → Option σ}
(hf : Primrec f)
:
theorem
Primrec.option_map
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → Option β}
{g : α → β → σ}
(hf : Primrec f)
(hg : Primrec₂ g)
:
Primrec fun (a : α) => Option.map (g a) (f a)
theorem
Primrec.option_map₁
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{f : α → σ}
(hf : Primrec f)
:
Primrec (Option.map f)
@[deprecated Primrec.option_getD_default (since := "2026-01-05")]
theorem
Primrec.bind_decode_iff
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → β → Option σ}
:
theorem
Primrec.map_decode_iff
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → β → σ}
:
theorem
Primrec.cond
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{c : α → Bool}
{f g : α → σ}
(hc : Primrec c)
(hf : Primrec f)
(hg : Primrec g)
:
Primrec fun (a : α) => bif c a then f a else g a
theorem
Primrec.ite
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{c : α → Prop}
[DecidablePred c]
{f g : α → σ}
(hc : PrimrecPred c)
(hf : Primrec f)
(hg : Primrec g)
:
theorem
PrimrecPred.not
{α : Type u_1}
[Primcodable α]
{p : α → Prop}
(hp : PrimrecPred p)
:
PrimrecPred fun (a : α) => ¬p a
theorem
PrimrecPred.and
{α : Type u_1}
[Primcodable α]
{p q : α → Prop}
(hp : PrimrecPred p)
(hq : PrimrecPred q)
:
PrimrecPred fun (a : α) => p a ∧ q a
theorem
PrimrecPred.or
{α : Type u_1}
[Primcodable α]
{p q : α → Prop}
(hp : PrimrecPred p)
(hq : PrimrecPred q)
:
PrimrecPred fun (a : α) => p a ∨ q a
theorem
Primrec.option_guard
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{p : α → β → Prop}
[DecidableRel p]
(hp : PrimrecRel p)
{f : α → β}
(hf : Primrec f)
:
Primrec fun (a : α) => Option.guard (fun (b : β) => decide (p a b)) (f a)
theorem
Primrec.list_findIdx₁
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{p : α → β → Bool}
(hp : Primrec₂ p)
(l : List β)
:
Primrec fun (a : α) => List.findIdx (p a) l
theorem
Primrec.list_idxOf₁
{α : Type u_1}
[Primcodable α]
[DecidableEq α]
(l : List α)
:
Primrec fun (a : α) => List.idxOf a l
theorem
Primrec.dom_finite
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
[Finite α]
(f : α → σ)
:
Primrec f
@[deprecated Primrec.dom_finite (since := "2025-08-23")]
theorem
Primrec.dom_fintype
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
[Finite α]
(f : α → σ)
:
Primrec f
Alias of Primrec.dom_finite.
def
Primrec.PrimrecBounded
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
(f : α → β)
:
A function is PrimrecBounded if its size is bounded by a primitive recursive function
Equations
- Primrec.PrimrecBounded f = ∃ (g : α → ℕ), Primrec g ∧ ∀ (x : α), Encodable.encode (f x) ≤ g x
Instances For
theorem
Primrec.nat_findGreatest
{α : Type u_1}
[Primcodable α]
{f : α → ℕ}
{p : α → ℕ → Prop}
[DecidableRel p]
(hf : Primrec f)
(hp : PrimrecRel p)
:
Primrec fun (x : α) => Nat.findGreatest (p x) (f x)
theorem
Primrec.of_graph
{α : Type u_1}
[Primcodable α]
{f : α → ℕ}
(h₁ : PrimrecBounded f)
(h₂ : PrimrecRel fun (a : α) (b : ℕ) => f a = b)
:
Primrec f
To show a function f : α → ℕ is primitive recursive, it is enough to show that the function
is bounded by a primitive recursive function and that its graph is primitive recursive
instance
Primcodable.sum
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
:
Primcodable (α ⊕ β)
Equations
- Primcodable.sum = { toEncodable := Sum.encodable, prim := ⋯ }
theorem
Primrec.sumCasesOn
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{σ : Type u_4}
[Primcodable α]
[Primcodable β]
[Primcodable γ]
[Primcodable σ]
{f : α → β ⊕ γ}
{g : α → β → σ}
{h : α → γ → σ}
(hf : Primrec f)
(hg : Primrec₂ g)
(hh : Primrec₂ h)
:
Primrec fun (a : α) => Sum.casesOn (f a) (g a) (h a)
theorem
PrimrecRel.not
{α : Type u_1}
{β : Type u_2}
{R : α → β → Prop}
[Primcodable α]
[Primcodable β]
(hf : PrimrecRel R)
:
PrimrecRel fun (a : α) (b : β) => ¬R a b
def
Primcodable.subtype
{α : Type u_1}
[Primcodable α]
{p : α → Prop}
[DecidablePred p]
(hp : PrimrecPred p)
:
Primcodable (Subtype p)
A subtype of a primitive recursive predicate is Primcodable.
Equations
- Primcodable.subtype hp = { toEncodable := Subtype.encodable, prim := ⋯ }
Instances For
Equations
- Primcodable.fin = Primcodable.ofEquiv { a : ℕ // id a < n } Fin.equivSubtype
theorem
Primcodable.mem_range_encode
{α : Type u_1}
[Primcodable α]
:
PrimrecPred fun (n : ℕ) => n ∈ Set.range Encodable.encode
Equations
theorem
Primrec.subtype_val
{α : Type u_1}
[Primcodable α]
{p : α → Prop}
[DecidablePred p]
{hp : PrimrecPred p}
:
theorem
Primrec.subtype_val_iff
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{p : β → Prop}
[DecidablePred p]
{hp : PrimrecPred p}
{f : α → Subtype p}
:
theorem
Primrec.subtype_mk
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{p : β → Prop}
[DecidablePred p]
{hp : PrimrecPred p}
{f : α → β}
{h : ∀ (a : α), p (f a)}
(hf : Primrec f)
:
theorem
Primrec.option_get
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{f : α → Option β}
{h : ∀ (a : α), (f a).isSome = true}
: