aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/specification
diff options
context:
space:
mode:
authorEduardo Julian2022-02-11 19:57:00 -0400
committerEduardo Julian2022-02-11 19:57:00 -0400
commit105ab334201646be6b594d3d1215297e3b629a10 (patch)
treed1f972d5fe676f8b93f4efa8fb0a8ce602878903 /stdlib/source/specification
parent469b171e5793422a4dbd27f4f2fab8a261c9ccf9 (diff)
Fixed directive extensions for Lux/Python.
Diffstat (limited to 'stdlib/source/specification')
-rw-r--r--stdlib/source/specification/lux/abstract/apply.lux78
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))