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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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