Mathlib Map

Structures · Lean core

Decidable

Either a proof that p is true or a proof that p is false. This is equivalent to a Bool paired with a proof that the Bool is true if and only if p is true. Decidable instances are primarily used via if-expressions and the tactic decide. In conditional expressions, the Decidable instance for the proposition is used to select a branch. At run time, this case distinction code is identical to that which would be generated for a Bool-based conditional. In proofs, the tactic decide synthesizes an instance of Decidable p, attempts to reduce it to isTrue h, and then succeeds with the proof h if it can. Because Decidable carries data, when writing @[simp] lemmas which include a Decidable instance on the LHS, it is best to use {_ : Decidable p} rather than [Decidable p] so that non-canonical instances can be found via unification rather than instance synthesis.

Defined in
Init.Prelude
Shape
One type argument, not a structure
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by1

Forgetful instances

Provided automatically by

Concrete types that are instances100

  • False
  • True
  • And
  • LE.le
  • LT.lt
  • Or
  • SimpleGraph.Connected
  • Fact
  • Iff
  • Membership.mem
  • Eq
  • Nat.Prime
  • Not
  • Monotone
  • Antitone
  • SimpleGraph.IsIndepSet
  • Set.BijOn
  • Polynomial.IsRoot
  • RBTree.RBNode.Ordered
  • Lists.Equiv
  • Sum.LiftRel
  • Irrational
  • String.Pos.IsAtEnd
  • Set.SurjOn
  • Exists
  • SimpleGraph.Walk.Nil
  • Std.Sat.CNF.Clause.Mem
  • Irreducible
  • Setoid.r
  • dite
  • Nat.Abundant
  • IsCompl
  • Nat.Pseudoperfect
  • Cycle.Nodup
  • List.IsChain
  • Set.InjOn
  • Ordnode.Emem
  • Multiset.Nodup
  • Function.IsPeriodicPt
  • List.Pairwise
  • UInt8.IsUTF8FirstByte
  • Matrix.IsHermitian
  • Array.Pairwise
  • Matrix.BlockTriangular
  • Nat.Coprime
  • Ordnode.All
  • String.Slice.Pos.IsAtEnd
  • Disjoint
  • Nat.ModEq
  • Relation.Map
  • Matrix.IsPivotedBy
  • List.IsPrefix
  • Finset.SupIndep
  • RBTree.RBNode.cmpLT
  • Std.HashMap.Equiv
  • Matrix.IsLeadingEntry
  • List.IsInfix
  • Quotient.liftOn
  • List.IsSuffix
  • MonotoneOn
  • Batteries.PairingHeapImp.Heap.NoSibling
  • SimpleGraph.IsClique
  • Nat.ProbablePrime
  • Std.HashSet.Equiv
  • Std.DTreeMap.Equiv
  • HasEquiv.Equiv
  • StrictAnti
  • ExistsUnique
  • IsConjRoot
  • Ordnode.Amem
  • Numbering.IsPrefix
  • ThreeAPFree
  • Codisjoint
  • List.Perm
  • Prod.lexLt
  • Nat.isPowerOfTwo
  • Stream'.Seq.TerminatedAt
  • List.Nodup
  • RBTree.RBNode.All
  • FP.ValidFinite
  • SimpleGraph.Walk.IsPath
  • HasSubset.Subset
  • Std.Http.URI.IsAllowedEncodedChars
  • RBTree.RBNode.Any
  • ByteArray.IsValidUTF8
  • SimpleGraph.IsNClique
  • Cycle.Nontrivial
  • String.Pos.Raw.IsValidForSlice
  • Quotient.liftOn₂
  • Std.Tactic.BVDecide.LRAT.Internal.Entails.eval
  • List.IsRotated
  • Polynomial.Monic
  • StrictAntiOn
  • Polynomial.TrailingMonic
  • IsLeast
  • Batteries.BinomialHeap.Imp.Heap.rankGT
  • StrictMonoOn
  • Dvd.dvd
  • Set.MapsTo
  • List.Lex

How is a type an instance?

Loading the hierarchy index…

Assumed by925

Ancestors0

No ancestors.