Theorem: TopM.get_unfold (MLIR/Semantics/Semantics.lean)

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
⊢ get τ name env =
    Except.ok
      (match SSAEnv.get name τ env with
        | some v => v
        | none => default,
        env)
Tactic:
simp [TopM.get]
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
⊢ bind StateT.get
      (fun s =>
        match SSAEnv.get name τ s with
        | some v => pure v
        | none => pure default)
      env =
    Except.ok
      (match SSAEnv.get name τ env with
        | some v => v
        | none => default,
        env)

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
⊢ bind StateT.get
      (fun s =>
        match SSAEnv.get name τ s with
        | some v => pure v
        | none => pure default)
      env =
    Except.ok
      (match SSAEnv.get name τ env with
        | some v => v
        | none => default,
        env)
Tactic:
simp_monad
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
⊢ (match SSAEnv.get name τ env with
      | some v => fun s => Except.ok (v, s)
      | none => fun s => Except.ok (default, s))
      env =
    Except.ok
      (match SSAEnv.get name τ env with
        | some v => v
        | none => default,
        env)

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
⊢ (match SSAEnv.get name τ env with
      | some v => fun s => Except.ok (v, s)
      | none => fun s => Except.ok (default, s))
      env =
    Except.ok
      (match SSAEnv.get name τ env with
        | some v => v
        | none => default,
        env)
Tactic:
cases (env.get name τ) <;> rfl
State after:
no goals