diff options
Diffstat (limited to 'stdlib/source/test/lux/type/check.lux')
| -rw-r--r-- | stdlib/source/test/lux/type/check.lux | 54 |
1 files changed, 27 insertions, 27 deletions
diff --git a/stdlib/source/test/lux/type/check.lux b/stdlib/source/test/lux/type/check.lux index 4674890ca..57ea22d70 100644 --- a/stdlib/source/test/lux/type/check.lux +++ b/stdlib/source/test/lux/type/check.lux @@ -89,11 +89,11 @@ #0)) (def: injection - (Injection (All [a] (/.Check a))) + (Injection (All (_ a) (/.Check a))) (\ /.monad in)) (def: comparison - (Comparison (All [a] (/.Check a))) + (Comparison (All (_ a) (/.Check a))) (function (_ == left right) (case [(/.result /.fresh_context left) (/.result /.fresh_context right)] [(#try.Success left) (#try.Success right)] @@ -314,7 +314,7 @@ )) (def: succeeds? - (All [a] (-> (/.Check a) Bit)) + (All (_ a) (-> (/.Check a) Bit)) (|>> (/.result /.fresh_context) (case> (#try.Success _) true @@ -323,7 +323,7 @@ false))) (def: fails? - (All [a] (-> (/.Check a) Bit)) + (All (_ a) (-> (/.Check a) Bit)) (|>> ..succeeds? not)) @@ -334,14 +334,14 @@ (in (#.Primitive name (list))))) (def: (non_twins = random) - (All [a] (-> (-> a a Bit) (Random a) (Random [a a]))) + (All (_ a) (-> (-> a a Bit) (Random a) (Random [a a]))) (do random.monad [left random right (random.only (|>> (= left) not) random)] (in [left right]))) (type: Super - (Ex [sub] [Text sub])) + (Ex (_ sub) [Text sub])) (type: Sub (Super Bit)) @@ -403,7 +403,7 @@ functions_have_covariant_outputs!))) (def: (verdict check) - (All [_] (-> (/.Check _) (/.Check Bit))) + (All (_ _) (-> (/.Check _) (/.Check Bit))) (function (_ context) (#try.Success [context (case (check context) (#try.Success _) @@ -526,28 +526,28 @@ (def: (handles_quantification! nominal) (-> Type Bit) (let [universals_satisfy_themselves! - (..succeeds? (/.check (.type (All [a] (Maybe a))) - (.type (All [a] (Maybe a))))) + (..succeeds? (/.check (.type (All (_ a) (Maybe a))) + (.type (All (_ a) (Maybe a))))) existentials_satisfy_themselves! - (..succeeds? (/.check (.type (Ex [a] (Maybe a))) - (.type (Ex [a] (Maybe a))))) + (..succeeds? (/.check (.type (Ex (_ a) (Maybe a))) + (.type (Ex (_ a) (Maybe a))))) universals_satisfy_particulars! (..succeeds? (/.check (.type (Maybe nominal)) - (.type (All [a] (Maybe a))))) + (.type (All (_ a) (Maybe a))))) particulars_do_not_satisfy_universals! - (..fails? (/.check (.type (All [a] (Maybe a))) + (..fails? (/.check (.type (All (_ a) (Maybe a))) (.type (Maybe nominal)))) particulars_satisfy_existentials! - (..succeeds? (/.check (.type (Ex [a] (Maybe a))) + (..succeeds? (/.check (.type (Ex (_ a) (Maybe a))) (.type (Maybe nominal)))) existentials_do_not_satisfy_particulars! (..fails? (/.check (.type (Maybe nominal)) - (.type (Ex [a] (Maybe a)))))] + (.type (Ex (_ a) (Maybe a)))))] (and universals_satisfy_themselves! existentials_satisfy_themselves! @@ -585,26 +585,26 @@ (def: (handles_application! nominal/0 nominal/1) (-> Type Type Bit) (let [types_flow_through! - (and (..succeeds? (/.check (.type ((All [a] a) nominal/0)) + (and (..succeeds? (/.check (.type ((All (_ a) a) nominal/0)) nominal/0)) (..succeeds? (/.check nominal/0 - (.type ((All [a] a) nominal/0)))) + (.type ((All (_ a) a) nominal/0)))) - (..succeeds? (/.check (.type ((Ex [a] a) nominal/0)) + (..succeeds? (/.check (.type ((Ex (_ a) a) nominal/0)) nominal/0)) (..succeeds? (/.check nominal/0 - (.type ((Ex [a] a) nominal/0))))) + (.type ((Ex (_ a) a) nominal/0))))) multiple_parameters! - (and (..succeeds? (/.check (.type ((All [a b] [a b]) nominal/0 nominal/1)) + (and (..succeeds? (/.check (.type ((All (_ a b) [a b]) nominal/0 nominal/1)) (.type [nominal/0 nominal/1]))) (..succeeds? (/.check (.type [nominal/0 nominal/1]) - (.type ((All [a b] [a b]) nominal/0 nominal/1)))) + (.type ((All (_ a b) [a b]) nominal/0 nominal/1)))) - (..succeeds? (/.check (.type ((Ex [a b] [a b]) nominal/0 nominal/1)) + (..succeeds? (/.check (.type ((Ex (_ a b) [a b]) nominal/0 nominal/1)) (.type [nominal/0 nominal/1]))) (..succeeds? (/.check (.type [nominal/0 nominal/1]) - (.type ((Ex [a b] [a b]) nominal/0 nominal/1)))))] + (.type ((Ex (_ a b) [a b]) nominal/0 nominal/1)))))] (and types_flow_through! multiple_parameters!))) @@ -798,10 +798,10 @@ (Random Bit) (do random.monad [example ..clean_type] - (in (and (and (/.subsumes? (.type (List example)) (.type (All [a] (List a)))) - (not (/.subsumes? (.type (All [a] (List a))) (.type (List example))))) - (and (/.subsumes? (.type (Ex [a] (List a))) (.type (List example))) - (not (/.subsumes? (.type (List example)) (.type (Ex [a] (List a)))))))))) + (in (and (and (/.subsumes? (.type (List example)) (.type (All (_ a) (List a)))) + (not (/.subsumes? (.type (All (_ a) (List a))) (.type (List example))))) + (and (/.subsumes? (.type (Ex (_ a) (List a))) (.type (List example))) + (not (/.subsumes? (.type (List example)) (.type (Ex (_ a) (List a)))))))))) (def: for_subsumption|named (Random Bit) |