Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Record.v Sprache: Coq

Original von: Coq^©

(* Nijmegen expects redefinition of sorts *)
Definition CProp := Prop.
Record test : CProp :=  {n : nat ; m : bool ; _ : n <> 0 }.
Require Import Program.
Require Import List.

Record vector {A : Type} {n : nat} := { vec_list : list A ; vec_len : length vec_list = n }.
Arguments vector : clear implicits.

Coercion vec_list : vector >-> list.

Hint Rewrite @vec_len : datatypes.

Ltac crush := repeat (program_simplify ; autorewrite with list datatypes ; auto with *).

Obligation Tactic := crush.

Program Definition vnil {A} : vector A 0 := {| vec_list := [] |}.

Program Definition vcons {A n} (a : A) (v : vector A n) : vector A (S n) :=
  {| vec_list := cons a (vec_list v) |}.

Hint Rewrite map_length rev_length : datatypes.

Program Definition vmap {A B n} (f : A -> B) (v : vector A n) : vector B n :=
  {| vec_list := map f v |}.

Program Definition vreverse {A n} (v : vector A n) : vector A n :=
  {| vec_list := rev v |}.

Fixpoint va_list {A B} (v : list (A -> B)) (w : list A) : list B :=
  match v, w with
    | nil, nil => nil
    | cons f fs, cons x xs => cons (f x) (va_list fs xs)
    | _, _ => nil
  end.

Program Definition va {A B n} (v : vector (A -> B) n) (w : vector A n) : vector B n :=
  {| vec_list := va_list v w |}.

Next Obligation.
  destruct v as [v Hv]; destruct w as [w Hw] ; simpl.
  subst n. revert w Hw. induction v ; destruct w ; crush.
  rewrite IHv ; auto.
Qed.

(* Correct type inference of record notation. Initial example by Spiwack. *)

Inductive Machin := {
Bazar : option Machin
}.

Definition bli : Machin :=
{| Bazar := Some ({| Bazar := None |}:Machin) |}.

Definition bli' : option (option Machin)  :=
Some (Some {| Bazar := None |} ).

Definition bli'' : Machin :=
{| Bazar := Some {| Bazar := None |} |}.

Definition bli''' := {| Bazar := Some {| Bazar := None |} |}.

(** Correctly use scoping information *)

Require Import ZArith.

Record Foo := { bar : Z }.
Definition foo := {| bar := 0 |}.

(** Notations inside records *)

Require Import Relation_Definitions.

Record DecidableOrder : Type :=
{ A : Type
; le : relation A where "x <= y" := (le x y)
; le_refl : reflexive _ le
; le_antisym : antisymmetric _ le
; le_trans : transitive _ le
; le_total : forall x y, {x <= y}+{y <= x}
}.

(* Test syntactic sugar suggested by wish report #2138 *)

Record R : Type := {
  P (A : Type) : Prop := exists x : A -> A, x = x;
  Q A : P A -> P A
}.

(* We allow reusing an implicit parameter named in non-recursive types *)
(* This is used in a couple of development such as UniMatch *)

Record S {A:Type} := { a : A; b : forall A:Type, A }.

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