Showing changes from revision #1 to #2: Added | Removed | Changed
Given a decidable strictly ordered set AA and terms a:Aa:A and b:Ab:A, an element c:Ac:A is strictly between aa and bb if (a<c)=1(a \lt c) = 1 and (c<b)=1(c \lt b) = 1 and a decidable open interval (a,b)(a, b) is a dependent type defined as
decidable strict order
decidable closed interval?
decidable lower bounded open interval?
decidable upper bounded open interval?
Revision on June 15, 2022 at 22:47:42 by Anonymous?. See the history of this page for a list of all contributions to it.