products/sources/formale sprachen/Isabelle/Tools/jEdit/dist/macros/Files/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: bug_4709.v   Sprache: Unknown


(** Bug 4709 https://coq.inria.fr/bug/4709
    Extraction wasn't reducing primitive projections in types. *)

Require Extraction.

Set Primitive Projections.

Record t := Foo { foo : Type }.
Definition ty := foo (Foo nat).

(* Without proper reduction of primitive projections in
   [extract_type], the type [ty] was extracted as [Tunknown].
   Let's check it isn't the case anymore. *)

Parameter check : nat.
Extract Constant check => "(O:ty)".
Extraction TestCompile ty check.

[ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ]