def Lean.Json.getObjValAs! (self : Json) (α : Type) (key : String) [Inhabited α] [FromJson α] : α

Equations

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

def Lean.Json.getObjValAsD (j : Json) (α : Type) [FromJson α] (k : String) (D : α) : Except String α

Turn non-existance of the key into default initialisation.

This silences ONLY the property not found: error. If the parsing of an existing value fails, we propagate the error.

Equations

• j.getObjValAsD α k D = match j.getObjVal? k with | Except.error a => pure D | Except.ok val => Lean.fromJson? val

def Lean.Json.getObjValAsD! (j : Json) (α : Type) [FromJson α] [Inhabited α] (k : String) : Except String α

getObjValAsD! = getObjValAsD default for inhabited types.

Equations

• j.getObjValAsD! α k = j.getObjValAsD α k default

def Lean.Json.getObjVals? (self : Json) (α β : Type) [Ord α] [FromJson α] [FromJson β] : Except String (Batteries.RBMap α β compare)

Equations

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

def Lean.Json.fromFile (path : System.FilePath) : IO Json

Equations

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

def EvmYul.UInt256.fromBlob? (blob : Blob) : Except String UInt256

Equations

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

def EvmYul.UInt256.fromBlob! (blob : Blob) : UInt256

Equations

• EvmYul.UInt256.fromBlob! blob = (EvmYul.UInt256.fromBlob? blob).toOption.get!

def EvmYul.Nat.fromBlob? (blob : Blob) : Except String ℕ

Equations

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

def EvmYul.AccountAddress.fromBlob? (s : Blob) : Except String AccountAddress

Equations

• EvmYul.AccountAddress.fromBlob? s = (fun (x : EvmYul.UInt256) => Fin.ofNat x.toNat) <$> EvmYul.UInt256.fromBlob? s

def EvmYul.AccountAddress.fromBlob! (blob : Blob) : AccountAddress

Equations

• EvmYul.AccountAddress.fromBlob! blob = (EvmYul.AccountAddress.fromBlob? blob).toOption.get!

unsafe def EvmYul.DebuggingAndProfiling.report {β : Type} {α : Sort u_1} [Inhabited β] (s : String) (f : α → β) (a : α) : β

Equations

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

def EvmYul.DebuggingAndProfiling.testJsonParser (α : Type) [Repr α] [Lean.FromJson α] (s : String) : String

Equations

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

def computeToList! {α : Type u_1} [LE α] [IsTrans α fun (x1 x2 : α) => x1 ≤ x2] [IsAntisymm α fun (x1 x2 : α) => x1 ≤ x2] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (m : Multiset α) : List α

Equations

• computeToList! m = Multiset.sort (fun (x1 x2 : α) => x1 ≤ x2) m

def Batteries.RBMap.partition {α β : Type} {cmp : α → α → Ordering} (t : RBMap α β cmp) (p : α → β → Bool) : RBMap α β cmp × RBMap α β cmp

Equations

• t.partition p = (t.filter p, t.filter fun (k : α) (v : β) => !p k v)

def Std.HashSet.diff {α : Type} [DecidableEq α] [Hashable α] (a b : HashSet α) : HashSet α

Equations

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