Mercurial > cpdt > repo

comparison src/GeneralRec.v @ 437:8077352044b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A pass over all formatting, after big pile of coqdoc changes
author Adam Chlipala <adam@chlipala.net>
date Fri, 27 Jul 2012 16:47:28 -0400
parents 5f25705a10ea
children cbfd23b4364d
comparison
equal deleted inserted replaced
436:5d5e44f905c7 437:8077352044b2
91 ]] 91 ]]
92 92
93 The bulk of the definitional work devolves to the%\index{accessibility relation}\index{Gallina terms!Acc}% _accessibility_ relation [Acc], whose definition we may also examine. *) 93 The bulk of the definitional work devolves to the%\index{accessibility relation}\index{Gallina terms!Acc}% _accessibility_ relation [Acc], whose definition we may also examine. *)
94 94
95 (* begin hide *) 95 (* begin hide *)
96 (* begin thide *)
96 Definition Acc_intro' := Acc_intro. 97 Definition Acc_intro' := Acc_intro.
98 (* end thide *)
97 (* end hide *) 99 (* end hide *)
98 100
99 Print Acc. 101 Print Acc.
100 (** %\vspace{-.15in}% [[ 102 (** %\vspace{-.15in}% [[
101 Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop := 103 Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop :=
750 752
751 Notation "x <- m1 ; m2" := 753 Notation "x <- m1 ; m2" :=
752 (TBind m1 (fun x => m2)) (right associativity, at level 70). 754 (TBind m1 (fun x => m2)) (right associativity, at level 70).
753 755
754 (* begin hide *) 756 (* begin hide *)
757 (* begin thide *)
755 Definition fib := pred. 758 Definition fib := pred.
759 (* end thide *)
756 (* end hide *) 760 (* end hide *)
757 761
758 (** %\vspace{-.15in}%[[ 762 (** %\vspace{-.15in}%[[
759 CoFixpoint fib (n : nat) : thunk nat := 763 CoFixpoint fib (n : nat) : thunk nat :=
760 match n with 764 match n with