Theorem: Array.init_zero (LeanSAT/Upstream/ToStd.lean)

State before:
α✝ : Type u_1
f : Fin 0 → α✝
⊢ init 0 f = #[]
Tactic:
simp [init, Id.run, forIn', Std.Range.forIn']
State after:
α✝ : Type u_1
f : Fin 0 → α✝
⊢ Std.Range.forIn'.loop { start := 0, stop := 0, step := 1 }.start { start := 0, stop := 0, step := 1 }.stop 1
      (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) 0 0 ⋯ #[] =
    #[]

State before:
α✝ : Type u_1
f : Fin 0 → α✝
⊢ Std.Range.forIn'.loop { start := 0, stop := 0, step := 1 }.start { start := 0, stop := 0, step := 1 }.stop 1
      (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) 0 0 ⋯ #[] =
    #[]
Tactic:
unfold Std.Range.forIn'.loop
State after:
α✝ : Type u_1
f : Fin 0 → α✝
⊢ (if hu : 0 < { start := 0, stop := 0, step := 1 }.stop then
      match 0 with
      | 0 => pure #[]
      | Nat.succ fuel => do
        let __do_lift ← ForInStep.yield (push #[] (f { val := 0, isLt := ⋯ }))
        match __do_lift with
          | ForInStep.done b => pure b
          | ForInStep.yield b =>
            Std.Range.forIn'.loop { start := 0, stop := 0, step := 1 }.start { start := 0, stop := 0, step := 1 }.stop 1
              (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) fuel (0 + 1) ⋯ b
    else pure #[]) =
    #[]

State before:
α✝ : Type u_1
f : Fin 0 → α✝
⊢ (if hu : 0 < { start := 0, stop := 0, step := 1 }.stop then
      match 0 with
      | 0 => pure #[]
      | Nat.succ fuel => do
        let __do_lift ← ForInStep.yield (push #[] (f { val := 0, isLt := ⋯ }))
        match __do_lift with
          | ForInStep.done b => pure b
          | ForInStep.yield b =>
            Std.Range.forIn'.loop { start := 0, stop := 0, step := 1 }.start { start := 0, stop := 0, step := 1 }.stop 1
              (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) fuel (0 + 1) ⋯ b
    else pure #[]) =
    #[]
Tactic:
simp
State after:
no goals