segfault2.lean

-- standard setup

lemma they_are_isomorphic (x : false) : ℕ = (ℕ × ℕ) :=
by contradiction

def repack (x : unit → false) (y : ℕ) : ℕ × ℕ :=
cast (they_are_isomorphic (x ())) y

def proj_nat (x : unit → false) : ℕ → ℕ :=
prod.fst ∘ repack x

-- now the new fun begins

def long_computation : ℕ → list ℕ
| 0     := [1,2,3]
| (n+1) := (long_computation n)^.reverse

vm_eval try_for 1 (long_computation 1000) -- none

-- but the kernel says something else:
meta example : try_for 1 (long_computation 1000) = some [1,2,3] := rfl

meta def crash (n : ℕ) : ℕ :=
let x := try_for 1 (long_computation 1000) in
if h : x = none then
  proj_nat (by contradiction) 4
else
  42

vm_eval crash 4