Documentation

EvmYul.Data.Stack

@[reducible, inline]

abbrev EvmYul.Stack (α : Type) :

Equations

EvmYul.Stack α = List α

Instances For

def EvmYul.Stack.new {α : Type} :

Equations

EvmYul.Stack.new = []

Instances For

def EvmYul.Stack.isEmpty {α : Type} (s : Stack α) :

Equations

s.isEmpty = List.isEmpty s

Instances For

def EvmYul.Stack.size {α : Type} (s : Stack α) :

Equations

s.size = List.length s

Instances For

def EvmYul.Stack.push {α : Type} (s : Stack α) (v : α) :

Equations

s.push v = v :: s

Instances For

def EvmYul.Stack.pop {α : Type} :

Stack α → Option (Stack α × α)

Equations

EvmYul.Stack.pop (hd :: tl) = some (tl, hd)
EvmYul.Stack.pop [] = none

Instances For

def EvmYul.Stack.pop2 {α : Type} :

Stack α → Option (Stack α × α × α)

Equations

EvmYul.Stack.pop2 (hd :: hd₁ :: tl) = some (tl, hd, hd₁)
x✝.pop2 = none

Instances For

def EvmYul.Stack.pop3 {α : Type} :

Stack α → Option (Stack α × α × α × α)

Equations

EvmYul.Stack.pop3 (hd :: hd₁ :: hd₂ :: tl) = some (tl, hd, hd₁, hd₂)
x✝.pop3 = none

Instances For

def EvmYul.Stack.pop4 {α : Type} :

Stack α → Option (Stack α × α × α × α × α)

Equations

EvmYul.Stack.pop4 (hd :: hd₁ :: hd₂ :: hd₃ :: tl) = some (tl, hd, hd₁, hd₂, hd₃)
x✝.pop4 = none

Instances For

def EvmYul.Stack.pop5 {α : Type} :

Stack α → Option (Stack α × α × α × α × α × α)

Equations

EvmYul.Stack.pop5 (hd :: hd₁ :: hd₂ :: hd₃ :: hd₄ :: tl) = some (tl, hd, hd₁, hd₂, hd₃, hd₄)
x✝.pop5 = none

Instances For

def EvmYul.Stack.pop6 {α : Type} :

Stack α → Option (Stack α × α × α × α × α × α × α)

Equations

EvmYul.Stack.pop6 (hd :: hd₁ :: hd₂ :: hd₃ :: hd₄ :: hd₅ :: tl) = some (tl, hd, hd₁, hd₂, hd₃, hd₄, hd₅)
x✝.pop6 = none

Instances For

def EvmYul.Stack.pop7 {α : Type} :

Stack α → Option (Stack α × α × α × α × α × α × α × α)

Equations

EvmYul.Stack.pop7 (hd :: hd₁ :: hd₂ :: hd₃ :: hd₄ :: hd₅ :: hd₆ :: tl) = some (tl, hd, hd₁, hd₂, hd₃, hd₄, hd₅, hd₆)
x✝.pop7 = none

Instances For

@[simp]

theorem EvmYul.Stack.isEmpty_push_false {α : Type} {x : α} {s : Stack α} :

(s.push x).isEmpty = false

@[simp]

theorem EvmYul.Stack.isEmpty_nil {α : Type} :

isEmpty [] = true

@[simp]

theorem EvmYul.Stack.isEmpty_cons_false {α : Type} {x : α} {s : Stack α} :

isEmpty (x :: s) = false

@[simp]

theorem EvmYul.Stack.size_nil {α : Type} :

@[simp]

theorem EvmYul.Stack.size_new {α : Type} :

@[simp]

theorem EvmYul.Stack.size_cons {α : Type} {x : α} {s : Stack α} :

size (x :: s) = s.size + 1

theorem EvmYul.Stack.size_zero_iff_isEmpty_eq_true {α : Type} {s : Stack α} :

s.size = 0 ↔ s.isEmpty = true

@[simp]

theorem EvmYul.Stack.size_push {α : Type} {x : α} {s : Stack α} :

(s.push x).size = s.size + 1

@[simp]

theorem EvmYul.Stack.pop_push {α : Type} {x : α} {s : Stack α} :

(s.push x).pop = some (s, x)

instance EvmYul.Stack.instInhabited {α : Type} :

Inhabited (Stack α)

Equations

EvmYul.Stack.instInhabited = { default := EvmYul.Stack.new }

instance EvmYul.Stack.instDecidableEq {α : Type} [DecidableEq α] :

DecidableEq (Stack α)

Equations

EvmYul.Stack.instDecidableEq = inferInstanceAs (DecidableEq (List α))

instance EvmYul.Stack.instEmptyCollection {α : Type} :

EmptyCollection (Stack α)

Equations

EvmYul.Stack.instEmptyCollection = { emptyCollection := EvmYul.Stack.new }

instance EvmYul.instToStringStack {α : Type} [ToString α] :

ToString (Stack α)

Equations

EvmYul.instToStringStack = inferInstanceAs (ToString (List α))