Documentation

Lean.Meta.HasNotBit

Utility functions around Nat.hasNotBit, used by sparse cases.

source
def mkHasNotBit (e : Lean.Expr) (ns : Array Nat) :
Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def mkHasNotBitProof (e : Lean.Expr) (ns : Array Nat) :
    Lean.MetaM Lean.Expr
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def isHasNotBit? (e : Lean.Expr) :
      Option Lean.Expr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def refutableHasNotBit? (e : Lean.Expr) :
        Lean.MetaM (Option Lean.Expr)

        Is e a hasNotBit type that can be refuted? Then return an expression that's the negation of it. (This is used by contradiction)

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For