類型綁定

類型邊界為類型規范添加條件。實現這一點的函數是守衛(守衛子句) 此功能可用于函數簽名、匿名函數簽名以及篩選類型 守衛寫在返回類型之后

謂詞

您可以使用返回 Bool 的表達式(謂詞表達式)指定變量滿足的條件 只能使用 值對象 和運算符。未來版本可能會支持編譯時函數

f a: [T; N] | T, N, N > 5 = ...
g a: [T; N | N > 5] | T, N = ...
Odd = {I: Int | I % 2 == 1}
R2Plus = {(L, R) | L, R: Ratio; L > 0 and R > 0}
GeneralizedOdd = {I | U; I <: Div(Nat, U); I % 2 == 0}