Mercurial > cpdt > repo
changeset 131:6bf40eff5e98
call-by-name is really call-by-need
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Wed, 22 Oct 2008 13:40:32 -0400 |
parents | 464db50b210a |
children | bc1f7d3687e7 |
files | src/Equality.v |
diffstat | 1 files changed, 1 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Equality.v Wed Oct 22 09:43:37 2008 -0400 +++ b/src/Equality.v Wed Oct 22 13:40:32 2008 -0400 @@ -37,7 +37,7 @@ (* begin thide *) (** 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. - 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. *) + 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. *) cbv delta. (** [[