← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to test-suite/success/Record.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
test-suite/success/Record.v
 
1
(* Nijmegen expects redefinition of sorts *)
 
2
Definition CProp := Prop.
 
3
Record test : CProp :=  {n : nat ; m : bool ; _ : n <> 0 }.
 
4
Require Import Program.
 
5
Require Import List.
 
6
 
 
7
Record vector {A : Type} {n : nat} := { vec_list : list A ; vec_len : length vec_list = n }.
 
8
Implicit Arguments vector [].
 
9
 
 
10
Coercion vec_list : vector >-> list.
 
11
 
 
12
Hint Rewrite @vec_len : datatypes.
 
13
 
 
14
Ltac crush := repeat (program_simplify ; autorewrite with list datatypes ; auto with *).
 
15
 
 
16
Obligation Tactic := crush.
 
17
 
 
18
Program Definition vnil {A} : vector A 0 := {| vec_list := [] |}.
 
19
 
 
20
Program Definition vcons {A n} (a : A) (v : vector A n) : vector A (S n) := 
 
21
  {| vec_list := cons a (vec_list v) |}.
 
22
 
 
23
Hint Rewrite map_length rev_length : datatypes.
 
24
 
 
25
Program Definition vmap {A B n} (f : A -> B) (v : vector A n) : vector B n := 
 
26
  {| vec_list := map f v |}.
 
27
 
 
28
Program Definition vreverse {A n} (v : vector A n) : vector A n := 
 
29
  {| vec_list := rev v |}.
 
30
 
 
31
Fixpoint va_list {A B} (v : list (A -> B)) (w : list A) : list B := 
 
32
  match v, w with
 
33
    | nil, nil => nil
 
34
    | cons f fs, cons x xs => cons (f x) (va_list fs xs)
 
35
    | _, _ => nil
 
36
  end.
 
37
 
 
38
Program Definition va {A B n} (v : vector (A -> B) n) (w : vector A n) : vector B n := 
 
39
  {| vec_list := va_list v w |}.
 
40
 
 
41
Next Obligation. 
 
42
  destruct v as [v Hv]; destruct w as [w Hw] ; simpl.
 
43
  subst n. revert w Hw. induction v ; destruct w ; crush. 
 
44
  rewrite IHv ; auto.
 
45
Qed.
 
46
 
 
47
(* Correct type inference of record notation. Initial example by Spiwack. *) 
 
48
 
 
49
Inductive Machin := {
 
50
 Bazar : option Machin
 
51
}.
 
52
 
 
53
Definition bli : Machin :=
 
54
 {| Bazar := Some ({| Bazar := None |}:Machin) |}.
 
55
 
 
56
Definition bli' : option (option Machin)  :=
 
57
 Some (Some {| Bazar := None |} ).
 
58
 
 
59
Definition bli'' : Machin :=
 
60
 {| Bazar := Some {| Bazar := None |} |}.
 
61
 
 
62
Definition bli''' := {| Bazar := Some {| Bazar := None |} |}.
 
63
 
 
64
(** Correctly use scoping information *)
 
65
 
 
66
Require Import ZArith.
 
67
 
 
68
Record Foo := { bar : Z }.
 
69
Definition foo := {| bar := 0 |}.
 
70
 
 
71
(** Notations inside records *)
 
72
 
 
73
Require Import Relation_Definitions.
 
74
 
 
75
Record DecidableOrder : Type :=
 
76
{ A : Type
 
77
; le : relation A where "x <= y" := (le x y)
 
78
; le_refl : reflexive _ le
 
79
; le_antisym : antisymmetric _ le
 
80
; le_trans : transitive _ le
 
81
; le_total : forall x y, {x <= y}+{y <= x}
 
82
}.