Theorems · Definition · logic and foundations
Encodable.decode
{α : Type u_1} → [self : Encodable α] → ℕ → Option αDecoding from ℕ to Option α
- Defined in
- Mathlib.Logic.Encodable.Basic
- Cited by
- 77 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- Encodable
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Encodablestatement and proof · cited by 140
Cited by104
Results whose statement or proof uses this declaration.
- Primrecproof · cited by 141
- Primrec.compproof · cited by 80
- Primrec.sndproof · cited by 66
- Primrec.fstproof · cited by 58
- Primrec.constproof · cited by 57
- Partrecproof · cited by 48
- Primrec.to_compproof · cited by 40
- Primrec.idproof · cited by 40
- Encodable.encodekstatement · cited by 27
- Encodable.decode₂proof · cited by 26
- Denumerable.ofNatproof · cited by 26
- Primrec.encode_iffproof · cited by 18