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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Omega0.v   Sprache: Unknown

(* L'algo d'inférence du prédicat doit gérer le K-rédex dans le type de b *)
(* Problème rapporté par Solange Coupet *)

Section A.

Variables (Alpha : Set) (Beta : Set).

Definition nodep_prod_of_dep (c : sigT (fun a : Alpha => Beta)) :
  Alpha * Beta := match c with
                  | existT _ a b => (a, b)
                  end.

End A.

[ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ]