Untersuchungsergebnis.fake Download desHaskell {Haskell[149] Fortran[373] Ada[376]}zum Wurzelverzeichnis wechseln
# 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
[ zur Elbe Produktseite wechseln0.81Quellennavigators
]
