Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Mod_params.v Sprache: Coq

Original von: Coq^©

(* Syntax test - all possible kinds of module parameters *)

Module Type SIG.
End SIG.

Module Type FSIG (X: SIG).
End FSIG.

Module F (X: SIG).
End F.

Module Q.
End Q.

(*
#trace Nametab.push;;
#trace Nametab.push_short_name;;
#trace Nametab.freeze;;
#trace Nametab.unfreeze;;
#trace Nametab.exists_cci;;
*)

Module M01. End M01.
Module M02 (X: SIG). End M02.
Module M03 (X Y: SIG). End M03.
Module M04 (X: SIG) (Y: SIG). End M04.
Module M05 (X Y: SIG) (Z1 Z: SIG). End M05.
Module M06 (X: SIG) (Y: SIG). End M06.
Module M07 (X Y: SIG) (Z1 Z: SIG). End M07.
Module M08 : SIG. End M08.
Module M09 (X: SIG) : SIG. End M09.
Module M10 (X Y: SIG) : SIG. End M10.
Module M11 (X: SIG) (Y: SIG) : SIG. End M11.
Module M12 (X Y: SIG) (Z1 Z: SIG) : SIG. End M12.
Module M13 (X: SIG) (Y: SIG) : SIG. End M13.
Module M14 (X Y: SIG) (Z1 Z: SIG) : SIG. End M14.
Module M15 := F Q.
Module M16 (X: FSIG) := X Q.
Module M17 (X Y: FSIG) := X Q.
Module M18 (X: FSIG) (Y: SIG) := X Y.
Module M19 (X Y: FSIG) (Z1 Z: SIG) := X Z.
Module M20 (X: FSIG) (Y: SIG) := X Y.
Module M21 (X Y: FSIG) (Z1 Z: SIG) := X Z.
Module M22 : SIG := F Q.
Module M23 (X: FSIG) : SIG := X Q.
Module M24 (X Y: FSIG) : SIG := X Q.
Module M25 (X: FSIG) (Y: SIG) : SIG := X Y.
Module M26 (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z.
Module M27 (X: FSIG) (Y: SIG) : SIG := X Y.
Module M28 (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z.

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.