The following is relevant to the BNF guys, with continously growing team
strength (according to Isabelle/aa7f051ba6ab).
Today we've had a tutorial with mostly fresh users, which is always useful
to see remaining snags. There were also 2-3 experienced Coq users, who
have the usual problems of a different kind: being stuck to Emacs or using
strange Window managers like Xmonad.
Examples for beginners usually use the list datatype, and the Prover IDE
makes it easy to find its definition. Many users started looking in the
HOL theories routinely, to get an idea how things are defined and how
proofs are done with them. Navigation makes the sources more accessible
and raises the demands for their quality. (I have ocasionally cleaned up
typical hyperlink target positions in Pure, to make them look more
obvious, if users happen to enter there.)
For the new high-end BNF version of 'a list there were a few funny
effects.
(1) Its definition looks terrific:
datatype_new (set: 'a) list (map: map rel: list_all2) =
=: Nil (defaults tl: "[]") ("[]")
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
It means it can no longer serve as example template for your own datatype
definitions. Note that I have already put the independent Seq.thy example
in a prominent place some years ago, to decouple basic examples from the
particularly difficult List.thy.
(2) Some users somehow used the "hd" and "tl" selector specifications
above as suggestion to define primitive recursive functions, e.g. like
this:
primref foo where
"foo [] = ..."
| "foo (Cons hd tl) = ..."
Of course this fails, since these are constants, not variables. It
results in type-inference errors that beginners find hard to understand,
and the Prover IDE has no position information about type errors yet.
(3) A genuine name space problem: "list" is concealed, and thus cannot be
completed in semantic completion.
Looking briefly through the sources, I merely found some odd workarounds
in BNF_Util.typedef -- it is usually worth investing the time to sort out
the fine points that lead to such complications and eliminate them:
(*TODO: is this really different from Typedef.add_typedef_global?*)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
