diff options
Diffstat (limited to '')
| -rw-r--r-- | stdlib/source/library/lux/type/refinement.lux | 24 |
1 files changed, 20 insertions, 4 deletions
diff --git a/stdlib/source/library/lux/type/refinement.lux b/stdlib/source/library/lux/type/refinement.lux index a34153800..0ea7bf75c 100644 --- a/stdlib/source/library/lux/type/refinement.lux +++ b/stdlib/source/library/lux/type/refinement.lux @@ -9,15 +9,16 @@ abstract]]]) (abstract: .public (Refined t %) - {#.doc "A refined type '%' of base type 't' using a predicate."} + {#.doc "A refined version of another type, using a predicate to select valid instances."} {#value t #predicate (Predicate t)} (type: .public (Refiner t %) + {#.doc (doc "A selection mechanism for refined instances of a type.")} (-> t (Maybe (Refined t %)))) - (def: .public (refinement predicate) + (def: .public (refiner predicate) (All [t] (Ex [%] (-> (Predicate t) (Refiner t %)))) @@ -37,6 +38,8 @@ ) (def: .public (lift transform) + {#.doc (doc "Yields a function that can work on refined values." + "Respects the constraints of the refinement.")} (All [t %] (-> (-> t t) (-> (Refined t %) (Maybe (Refined t %))))) @@ -50,7 +53,8 @@ ) (def: .public (only refiner values) - (All [t %] (-> (Refiner t %) (List t) (List (Refined t %)))) + (All [t %] + (-> (Refiner t %) (List t) (List (Refined t %)))) (case values #.End #.End @@ -64,7 +68,9 @@ (only refiner tail)))) (def: .public (partition refiner values) - (All [t %] (-> (Refiner t %) (List t) [(List (Refined t %)) (List t)])) + {#.doc (doc "Separates refined values from the un-refined ones.")} + (All [t %] + (-> (Refiner t %) (List t) [(List (Refined t %)) (List t)])) (case values #.End [#.End #.End] @@ -81,6 +87,16 @@ (#.Item head no)])))) (syntax: .public (type refiner) + {#.doc (doc "The Refined type associated with a Refiner type." + (def: even + (refiner even?)) + + (def: Even + Type + (type even)) + + (: (Maybe Even) + (even 123)))} (macro.with_gensyms [g!t g!%] (in (list (` ((~! type.:by_example) [(~ g!t) (~ g!%)] (..Refiner (~ g!t) (~ g!%)) |