Re: [isabelle-dev] HOL-Probability broken
I’ve pushed a correction to that particular problem.
I’ve no time to verify that there are no further problems. Sorry again.
Larry
On 17 Mar 2015, at 17:22, Makarius makar...@sketis.net wrote:
In Isabelle/cd945dc13bec HOL-Probability is broken:
*** Now trying to infer coercions globally.
***
*** Coercion inference failed:
*** uncomparable types in type list
***
*** Cannot fulfil subtype constraints:
*** ??'a : ereal from function application
*** \integral\^sup+ x. ereal (x ^ k * exp (- x)) *
***indicator {0::??'i..} x
***\partiallborel =
*** fact k
*** ereal : ereal from function application
*** op =
*** (\integral\^sup+ x. ereal (x ^ k * exp (- x)) *
*** indicator {0::??'h..} x
*** \partiallborel)
*** nat = ??'a : ??'b = ??'c from function application
*** fact::??'b = ??'c
*** At command lemma (line 116 of
~~/src/HOL/Probability/Distributions.thy)
The problem might be an untested merge by Larry, but I did not make more
detailed tests to prove that hypothesis.
What is also odd: http://isabelle.in.tum.de/reports/Isabelle does not show
any activity nor results of testing. Maybe the mira service is down?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] HOL-Probability broken
In Isabelle/cd945dc13bec HOL-Probability is broken:
*** Now trying to infer coercions globally.
***
*** Coercion inference failed:
*** uncomparable types in type list
***
*** Cannot fulfil subtype constraints:
*** ??'a : ereal from function application
*** \integral\^sup+ x. ereal (x ^ k * exp (- x)) *
***indicator {0::??'i..} x
***\partiallborel =
*** fact k
*** ereal : ereal from function application
*** op =
*** (\integral\^sup+ x. ereal (x ^ k * exp (- x)) *
*** indicator {0::??'h..} x
*** \partiallborel)
*** nat = ??'a : ??'b = ??'c from function application
*** fact::??'b = ??'c
*** At command lemma (line 116 of ~~/src/HOL/Probability/Distributions.thy)
The problem might be an untested merge by Larry, but I did not make more
detailed tests to prove that hypothesis.
What is also odd: http://isabelle.in.tum.de/reports/Isabelle does not show
any activity nor results of testing. Maybe the mira service is down?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Probability broken
Sorry, I don’t know how that one slipped through.
I test on my own machine.
Larry
On 17 Mar 2015, at 17:22, Makarius makar...@sketis.net wrote:
In Isabelle/cd945dc13bec HOL-Probability is broken:
*** Now trying to infer coercions globally.
***
*** Coercion inference failed:
*** uncomparable types in type list
***
*** Cannot fulfil subtype constraints:
*** ??'a : ereal from function application
*** \integral\^sup+ x. ereal (x ^ k * exp (- x)) *
***indicator {0::??'i..} x
***\partiallborel =
*** fact k
*** ereal : ereal from function application
*** op =
*** (\integral\^sup+ x. ereal (x ^ k * exp (- x)) *
*** indicator {0::??'h..} x
*** \partiallborel)
*** nat = ??'a : ??'b = ??'c from function application
*** fact::??'b = ??'c
*** At command lemma (line 116 of
~~/src/HOL/Probability/Distributions.thy)
The problem might be an untested merge by Larry, but I did not make more
detailed tests to prove that hypothesis.
What is also odd: http://isabelle.in.tum.de/reports/Isabelle does not show
any activity nor results of testing. Maybe the mira service is down?
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
