1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
# Script simulating a dialog between coqide 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 Coq.extraction.Extraction. }
ADD { Require Import List. }
ADD { Import ListNotations. }
ADD { Definition myrev{A}(l : list A) : {rl : list A | rl = rev 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
|
