products/sources/formale sprachen/Coq/test-suite/ide/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Well_Ordering.v   Sprache: Coq

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.73Quellennavigators  ]