products/sources/formale Sprachen/Coq/test-suite/output/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Inductive.out   Sprache: Unknown

Spracherkennung für: .out vermutete Sprache: Haskell {Haskell[404] CS[665] Ada[703]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]

The command has indeed failed with message:
Last occurrence of "list'" must have "A" as 1st argument in
 "A -> list' A -> list' (A * A)%type".
Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x

For foo: Argument scopes are [type_scope _]
For Foo: Argument scopes are [type_scope _]

[ Dauer der Verarbeitung: 0.63 Sekunden  ]