Mercurial > cpdt > repo

comparison src/Equality.v @ 131:6bf40eff5e98

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
call-by-name is really call-by-need
author Adam Chlipala <adamc@hcoop.net>
date Wed, 22 Oct 2008 13:40:32 -0400
parents 0bfc75502498
children bc1f7d3687e7
comparison
equal deleted inserted replaced
130:464db50b210a 131:6bf40eff5e98
35 35
36 Theorem reduce_me : pred' 1 = 0. 36 Theorem reduce_me : pred' 1 = 0.
37 (* begin thide *) 37 (* begin thide *)
38 (** CIC follows the traditions of lambda calculus in associating reduction rules with Greek letters. Coq can certainly be said to support the familiar alpha reduction rule, which allows capture-avoiding renaming of bound variables, but we never need to apply alpha explicitly, since Coq uses a de Bruijn representation that encodes terms canonically. 38 (** CIC follows the traditions of lambda calculus in associating reduction rules with Greek letters. Coq can certainly be said to support the familiar alpha reduction rule, which allows capture-avoiding renaming of bound variables, but we never need to apply alpha explicitly, since Coq uses a de Bruijn representation that encodes terms canonically.
39 39
40 The delta rule is for unfolding global definitions. We can use it here to unfold the definition of [pred']. We do this with the [cbv] tactic, which takes a list of reduction rules and makes as many call-by-value reduction steps as possible, using only those rules. There is an analogous tactic [lazy] for call-by-name reduction. *) 40 The delta rule is for unfolding global definitions. We can use it here to unfold the definition of [pred']. We do this with the [cbv] tactic, which takes a list of reduction rules and makes as many call-by-value reduction steps as possible, using only those rules. There is an analogous tactic [lazy] for call-by-need reduction. *)
41 41
42 cbv delta. 42 cbv delta.
43 (** [[ 43 (** [[
44 44
45 ============================ 45 ============================