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

def Lean.mkHasNotBit (e : Expr) (ns : Array Nat) : Expr

Equations

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

def Lean.mkHasNotBitProof (e : Expr) (ns : Array Nat) : MetaM Expr

Equations

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

def Lean.isHasNotBit? (e : Expr) : Option Expr

Equations

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

def Lean.refutableHasNotBit? (e : Expr) : MetaM (Option 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.