[isabelle] Malformed dependency error with overloading



Dear Isabelle experts,

For the attached theory, Isabelle2016 yields the following error, which I do not understand at all.

Malformed dependency of test('a) -> sample(bool, 'a)
(restriction sample('a, ('b, 'c) envT) from "TEst.sample_envT_def_raw")
The error(s) above occurred in definition "test_def_raw":
  "test â sample my_pmf"

Why is the definition rejected? What could possibly go wrong here? What are the requirements on a well-formed dependency? Section 5.10 of the Isabelle2016 Isar-Ref manual does not say much about those dependency checks.

Best,
Andreas

Attachment: TEst.thy
Description: application/extension-thy



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