Mathlib Map

Structures · Logic and sets

Encodable

Constructively countable type. Made from an explicit injection encode : α → ℕ and a partial inverse decode : ℕ → Option α. Note that finite types are countable. See Denumerable if you wish to enforce infiniteness.

Defined in
Mathlib.Logic.Encodable.Basic
Shape
One type argument · adds encode, decode, encodek
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by3

Forgetful instances

Every Encodable is also a

Provided automatically by

Concrete types that are instances27

  • Int
  • Nat
  • Rat
  • Bool
  • NNRat
  • Finsupp
  • DFinsupp
  • PNat
  • WType
  • List.Vector
  • FirstOrder.Language.Term
  • ULower
  • _private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S
  • Subtype
  • Prod
  • Set.Elem
  • ULift
  • Fin
  • PUnit
  • Sum
  • List
  • Sigma
  • Multiset
  • Finset
  • Option
  • PLift
  • Array

How is a type an instance?

Loading the hierarchy index…

Assumed by168

Ancestors3