Quelle bug_2584.v Sprache: Coq

Set Implicit Arguments.

Definition err : Type := unit.

Inductive res (A: Type) : Type :=
| OK: A -> res A
| Error: err -> res A.

Arguments Error [A].

Set Printing Universes.

Section FOO.

Inductive ftyp : Type :=
  | Funit : ftyp
  | Ffun : list ftyp -> ftyp
  | Fref : area -> ftyp
with area : Type :=
  | Stored : ftyp -> area
.

Print ftyp.
(* yields:
Inductive ftyp : Type (* Top.27429 *)
    Funit : ftyp | Ffun : list ftyp -> ftyp | Fref : area -> ftyp
  with area : Type (* Set *) :=  Stored : ftyp -> area
*)

Fixpoint tc_wf_type (ftype: ftyp) {struct ftype}: res unit :=
  match ftype with
    | Funit => OK tt
    | Ffun args =>
       ((fix tc_wf_types (ftypes: list ftyp){struct ftypes}: res unit :=
           match ftypes with
             | nil => OK tt
             | cons t ts =>
                 match tc_wf_type t with
                   | OK tt => tc_wf_types ts
                   | Error m => Error m
                 end
           end) args)
     | Fref a => tc_wf_area a
   end
with tc_wf_area (ar:area): res unit :=
  match ar with
    | Stored c => tc_wf_type c
  end.

End FOO.

Print ftyp.
(* yields:
Inductive ftyp : Type (* Top.27465 *)
    Funit : ftyp | Ffun : list ftyp -> ftyp | Fref : area -> ftyp
  with area : Set :=  Stored : ftyp -> area
*)

Fixpoint tc_wf_type' (ftype: ftyp) {struct ftype}: res unit :=
  match ftype with
    | Funit => OK tt
    | Ffun args =>
       ((fix tc_wf_types (ftypes: list ftyp){struct ftypes}: res unit :=
           match ftypes with
             | nil => OK tt
             | cons t ts =>
                 match tc_wf_type' t with
                   | OK tt => tc_wf_types ts
                   | Error m => Error m
                 end
           end) args)
     | Fref a => tc_wf_area' a
   end
with tc_wf_area' (ar:area): res unit :=
  match ar with
    | Stored c => tc_wf_type' c
  end.

(* yields:
Error:
Incorrect elimination of "ar" in the inductive type "area":
the return type has sort "Type (* max(Set, Top.27424) *)
should be "Prop" or "Set".
Elimination of an inductive object of sort Set
is not allowed on a predicate in sort Type
because strong elimination on non-small inductive types leads to paradoxes.
*)

quality98%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.