The Coq mailing list

["Lukasz Stafiniak" <l_stafiniak AT hoga.pl>]

Hi List fellows,

1st - a proposal

I propose that the proof-by-pointing engine
is included into the standard distribution of Coq.
It could be done like this: written entirely in
OCaml+Tcl/Tk, compiled with (or dynamically
loaded to) Coq toplevel, called as a command
while in proof-mode, when leaving proof-by-pointing
(after as many proof steps as one wishes) shall
output a script of the tactics that actually were
performed (this script to be inserted into poof
script managed by ProofGeneral, if one uses it).

2nd - a question

What is the difference between Set and Type, if
not depending explicitely on their position in type
hierarchy? Why shouldn't reals be axiomatised in
Set? (What means "continuity" in type (or domain,
or category) theory?)

Thanks for your attention,
Cheers!
Lukasz Stafiniak

PS. Sorry for these below, I'll soon get rid of it...



------------------------------------------------------------
Ju¿ wkrótce w sprzeda¿y nowa wersja programu mks_vir 2003 !!!
wiêcej informacji na temat nowej  wersji 2003 na stronie : www.mks.com.pl