diff options
author | Eduardo Julian | 2022-02-11 19:57:00 -0400 |
---|---|---|
committer | Eduardo Julian | 2022-02-11 19:57:00 -0400 |
commit | 105ab334201646be6b594d3d1215297e3b629a10 (patch) | |
tree | d1f972d5fe676f8b93f4efa8fb0a8ce602878903 /stdlib/source/specification | |
parent | 469b171e5793422a4dbd27f4f2fab8a261c9ccf9 (diff) |
Fixed directive extensions for Lux/Python.
Diffstat (limited to 'stdlib/source/specification')
-rw-r--r-- | stdlib/source/specification/lux/abstract/apply.lux | 78 |
1 files changed, 41 insertions, 37 deletions
diff --git a/stdlib/source/specification/lux/abstract/apply.lux b/stdlib/source/specification/lux/abstract/apply.lux index 867a7b76f..3d01a1217 100644 --- a/stdlib/source/specification/lux/abstract/apply.lux +++ b/stdlib/source/specification/lux/abstract/apply.lux @@ -1,65 +1,69 @@ (.using - [library - [lux "*" - ["_" test {"+" Test}] - [abstract - [monad {"+" do}]] - [control - ["[0]" function]] - [math - ["[0]" random] - [number - ["n" nat]]]]] - [\\library - ["[0]" / {"+" Apply}]] - [// - [functor {"+" Injection Comparison}]]) + [library + [lux "*" + ["_" test {"+" Test}] + [abstract + [monad {"+" do}]] + [control + ["[0]" function]] + [math + ["[0]" random {"+" Random}] + [number + ["n" nat]]]]] + [\\library + ["[0]" / {"+" Apply}]] + [// + [functor {"+" Injection Comparison}]]) -(def: (identity injection comparison (^open "#[0]")) +(def: (identity injection comparison (^open "/#[0]")) (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test)) (do [! random.monad] [sample (# ! each injection random.nat)] (_.test "Identity." ((comparison n.=) - (#on sample (injection function.identity)) + (/#on sample (injection function.identity)) sample)))) -(def: (homomorphism injection comparison (^open "#[0]")) +(def: (homomorphism injection comparison (^open "/#[0]")) (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test)) (do [! random.monad] [sample random.nat increase (# ! each n.+ random.nat)] (_.test "Homomorphism." ((comparison n.=) - (#on (injection sample) (injection increase)) + (/#on (injection sample) (injection increase)) (injection (increase sample)))))) -(def: (interchange injection comparison (^open "#[0]")) +(def: (interchange injection comparison (^open "/#[0]")) (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test)) (do [! random.monad] [sample random.nat increase (# ! each n.+ random.nat)] (_.test "Interchange." ((comparison n.=) - (#on (injection sample) (injection increase)) - (#on (injection increase) (injection (: (-> (-> Nat Nat) Nat) - (function (_ f) (f sample))))))))) + (/#on (injection sample) (injection increase)) + (/#on (injection increase) (injection (: (-> (-> Nat Nat) Nat) + (function (_ f) (f sample))))))))) -(def: (composition injection comparison (^open "#[0]")) +(def: (composition injection comparison (^open "/#[0]")) (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test)) - (do [! random.monad] - [sample random.nat - increase (# ! each n.+ random.nat) - decrease (# ! each n.- random.nat)] - (_.test "Composition." - ((comparison n.=) - (|> (injection function.composite) - (#on (injection increase)) - (#on (injection decrease)) - (#on (injection sample))) - (#on (#on (injection sample) - (injection increase)) - (injection decrease)))))) + (:let [:$/1: (-> Nat Nat)] + (do [! random.monad] + [sample random.nat + increase (: (Random :$/1:) + (# ! each n.+ random.nat)) + decrease (: (Random :$/1:) + (# ! each n.- random.nat))] + (_.test "Composition." + ((comparison n.=) + (|> (injection (: (-> :$/1: :$/1: :$/1:) + function.composite)) + (/#on (injection increase)) + (/#on (injection decrease)) + (/#on (injection sample))) + (/#on (/#on (injection sample) + (injection increase)) + (injection decrease))))))) (def: .public (spec injection comparison apply) (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test)) |