Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bug_3810.v Sprache: Coq

Original von: Coq^©

(* Computation of dependencies in the "match" return predicate was incomplete *)
(* Submitted by R. O'Connor, Nov 2009 *)

Inductive Symbol : Set :=
| VAR : Symbol.

Inductive SExpression :=
| atomic : Symbol -> SExpression.

Inductive ProperExpr : SExpression -> SExpression -> Type :=
| pe_3 : forall (x : Symbol) (alpha : SExpression),
    ProperExpr alpha (atomic VAR) ->
    ProperExpr (atomic x) alpha.

Definition A (P : forall s : SExpression, Type)
(x alpha alpha1 : SExpression)
(t : ProperExpr (x) alpha1) : option (x = atomic VAR) :=
match t as pe in ProperExpr a b return option (a = atomic VAR) with
| pe_3 x0 alpha3 tye' =>
      (fun (x:Symbol) (alpha : SExpression) => @None (atomic x = atomic VAR))
       x0 alpha3
end.

Definition B (P : forall s : SExpression, Type)
(x alpha alpha1 : SExpression)
(t : ProperExpr (x) alpha1) : option (x = atomic VAR) :=
match t as pe in ProperExpr a b return option (a = atomic VAR) with
| pe_3 x0 alpha3 tye' =>
      (fun (x:Symbol) (alpha : SExpression) (t:ProperExpr alpha (atomic VAR)) => @None (atomic x = atomic VAR))
       x0 alpha3 tye'
end.

¤ Dauer der Verarbeitung: 0.30 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.