Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: obsq3a.cob Sprache: Coq

Original von: Coq^©

Require Import List.
Require Import Arith.
Require Import Recdef.
Require Import Omega.

Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
  match xys with
    | (nil, _) => snd xys
    | (_, nil) => fst xys
    | (x :: xs', y :: ys') => match Nat.compare x y with
                                | Lt => x :: foo (xs', y :: ys')
                                | Eq => x :: foo (xs', ys')
                                | Gt => y :: foo (x :: xs', ys')
                              end
  end.
Proof.
  intros; simpl; omega.
  intros; simpl; omega.
  intros; simpl; omega.
Qed.

Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
  let (xs, ys) := xys in
  match (xs, ys) with
    | (nil, _) => ys
    | (_, nil) => xs
    | (x :: xs', y :: ys') => match Nat.compare x y with
                                | Lt => x :: foo (xs', ys)
                                | Eq => x :: foo (xs', ys')
                                | Gt => y :: foo (xs, ys')
                              end
  end.

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

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.