Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: coq_omega.mli Sprache: Coq

Original von: Coq^©

(* This example was proposed by Cuihtlauac ALVARADO *)

Require Import List.

Fixpoint mult2 (n : nat) : nat :=
  match n with
  | O => 0
  | S n => S (S (mult2 n))
  end.

Inductive list : nat -> Set :=
  | nil : list 0
  | cons : forall n : nat, list (mult2 n) -> list (S (S (mult2 n))).

Type
  (fun (P : forall n : nat, list n -> Prop) (f : P 0 nil)
     (f0 : forall (n : nat) (l : list (mult2 n)),
           P (mult2 n) l -> P (S (S (mult2 n))) (cons n l)) =>
   fix F (n : nat) (l : list n) {struct l} : P n l :=
     match l as x0 in (list x) return (P x x0) with
     | nil => f
     | cons n0 l0 => f0 n0 l0 (F (mult2 n0) l0)
     end).

Inductive list' : nat -> Set :=
  | nil' : list' 0
  | cons' : forall n : nat, let m := mult2 n in list' m -> list' (S (S m)).

Fixpoint length n (l : list' n) {struct l} : nat :=
  match l with
  | nil' => 0
  | cons' _ m l0 => S (length m l0)
  end.

Type
  (fun (P : forall n : nat, list' n -> Prop) (f : P 0 nil')
     (f0 : forall n : nat,
           let m := mult2 n in
           forall l : list' m, P m l -> P (S (S m)) (cons' n l)) =>
   fix F (n : nat) (l : list' n) {struct l} : P n l :=
     match l as x0 in (list' x) return (P x x0) with
     | nil' => f
     | cons' n0 m l0 => f0 n0 l0 (F m l0)
     end).

(* Check on-the-fly insertion of let-in patterns for compatibility *)

Inductive list'' : nat -> Set :=
  | nil'' : list'' 0
  | cons'' :
      forall n : nat,
      let m := mult2 n in list'' m -> let p := S (S m) in list'' p.

Check
  (fix length n (l : list'' n) {struct l} : nat :=
     match l with
     | nil'' => 0
     | cons'' n l0 => S (length (mult2 n) l0)
     end).

(* Check let-in in both parameters and in constructors *)

Inductive list''' (A:Set) (B:=(A*A)%type) (a:A) : B -> Set :=
  | nil''' : list''' A a (a,a)
  | cons''' :
     forall a' : A, let m := (a',a) in list''' A a m -> list''' A a (a,a).

Fixpoint length''' (A:Set) (B:=(A*A)%type) (a:A) (m:B) (l:list''' A a m)
  {struct l} : nat :=
  match l with
  | nil''' _ _ => 0
  | @cons''' _ _ _ _ m l0 => S (length''' A a m l0)
  end.

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht 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.