# Script simulating a dialog between rocqide and coqtop -ideslave
# Run it via fake_ide
#
# Extraction will force the future computation, assert it is blocking
# Example courtesy of Jonathan (jonikelee)
#
ADD { Require Corelib.extraction.Extraction. }
ADD { Require Import ListDef. }
ADD { Fixpoint rev A (l:list A) : list A := match l with nil => nil | x :: l' => rev A l' ++ cons x nil end. }
ADD { Definition myrev{A}(l : list A) : {rl : list A | rl = rev A l}. }
ADD { Proof. }
ADD {   induction l. }
ADD {    eexists; reflexivity. }
ADD {    cbn; destruct IHl as [rl' H]; rewrite <-H; eexists; reflexivity. }
ADD { Qed. }
ADD { Extraction myrev. }
GOALS