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.