Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Pervasives or Printf module ?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2006-01-23 (09:18)
From: Remi Vanicat <remi.vanicat@g...>
Subject: Re: [Caml-list] Re: Pervasives or Printf module ?
2006/1/22, Vincenzo Ciancia <>:
> Jon Harrop wrote:
> > To get the latter to act as the former
> > does, you must beta expand (I think that is the correct technical term)
> In computer science literature, alpha conversion is usually the renaming of
> a bound variable (fun x -> T = fun y -> T[y/x] provided that y does not
> occurr in T), beta _reduction_ is function application ((fun x -> T)(T') =
> T[T'/x]) , and _eta_ expansion is the term rewriting you're looking for.
> I don't know why, maybe it's just the order in which they were enumerated
> originarily, but where are gamma, delta, epsilon, zeta rewrite rules? :)

In the coq manual, one can see severall other rewriting rule, like
iota-reduction, delta-reduction and zeta-reduction.