Re: [isabelle] Strange interaction between ambiguous syntax and dummy patterns

Hi Bertram,

> For example, using the following two artificial data declarations,
>   datatype o1 = O1 unit unit (infixr "?" 70)
>   datatype o2 = O2 unit unit (infixr "?" 70)
> the following function declaration is accepted with an ambiguity
> warning,
>   fun ok :: "o1 â unit option â o2" where
>     "ok (a ? b) (Some c) = () ? ()"
> but after replacing the unused 'c' variable by a dummy pattern, an
> error is produced.
>   fun fail1 :: "o1 â unit option â unit" where
>     "fail1 (a ? b) (Some _) = ()"

I guess dummy parameters are treated differently during type inference.

Maybe this is just an accidental behaviour, but I do not know the details.

Generally, over the last years there has been the tendency to avoid
ambiguous syntax altogether, e.g. using ad-hoc overloading etc.
Isabelle symbols give you access to plenty of unicode glyphs which can
offer alternatives.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.