Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] real number calculation

view this post on Zulip Email Gateway (Aug 17 2022 at 13:28):

From: nipkow@in.tum.de

Also, how to express the pre-condition that "a is within the area [0,1]"?

You could just write "0 <= a & a <= 1". Aternatively, there is a theory of
intervals (SetInterval.thy) that provides the necessary notation, in this
case "a : {0..1}".

Tobias

Last updated: May 03 2024 at 08:18 UTC