The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

             Alternatively,
>             Program could provide means of importing the base
>             functionality without
>             needlessly importing modules. What do you think?
> 
> 
>     But then how different is this from refine ?
> 
> 
> |Program| uses a bidirectional type-inference mechanism. This is the
> main use of |Program| for me: a cleaner and bidirectional |refine|
> (cleaner in the sense that visually |Program Definition foo : type :=
> term.| is nicer than |Definition foo : type. refine (term).|).

Right. Also, "Obligations tactic" can be used to easily automatically
solve goals, so we can entirely hide the "proof block", and use
"Program" features even when stating a Lemma, which is AFAIK not
possible with "refine".

Furthermore, with "Program", one doesn't have to state the entire type
even if one has holes in the term, while "Definition ... refine" forces
one to write down the type. (Or maybe that's what you meant by
"bidirectional" above.)

Kind regards,
Ralf