Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: sm206a.cob Sprache: Coq

Original von: Coq^©

(* Check injection in presence of dependencies hidden in applicative terms *)

Inductive TupleT : nat -> Type :=
  nilT : TupleT 0
| consT {n} A : (A -> TupleT n) -> TupleT (S n).

Inductive Tuple : forall n, TupleT n -> Type :=
  nil : Tuple _ nilT
| cons {n} A (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F).

Goal forall n A F x X n0 A0 x0 F0 H0 (H : existT (fun n0 : nat => {H0 : TupleT
n0 & Tuple n0 H0})
         (S n0)
         (existT (fun H0 : TupleT (S n0) => Tuple (S n0) H0)
            (consT A0 F0) (cons A0 x0 F0 H0)) =
       existT (fun n0 : nat => {H0 : TupleT n0 & Tuple n0 H0})
         (S n)
         (existT (fun H0 : TupleT (S n) => Tuple (S n) H0)
            (consT A F) (cons A x F X))), False.
intros.
injection H.
Abort.

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