@@ -128,24 +128,27 @@ mapIsJust = constrained' $ \ [var| x |] [var| y |] ->
128128
129129eitherKeys :: Specification ([Int ], [Int ], Map (Either Int Int ) Int )
130130eitherKeys = constrained' $ \ [var | as |] [var | bs |] [var | m |] ->
131- [
132- forAll' m $ \ [ var | k |] _v ->
133- [ caseOn k
134- (branch $ \ a -> a `elem_` as)
135- (branch $ \ b -> b `elem_` bs)
136- , reify as (map Left ) $ \ ls ->
137- reify bs (map Right ) $ \ rs ->
138- k `elem_` ls ++. rs
131+ [ forAll' m $ \ [ var | k |] _v ->
132+ [ caseOn
133+ k
134+ (branch $ \ a -> a `elem_` as)
135+ (branch $ \ b -> b `elem_` bs)
136+ , reify as (map Left ) $ \ ls ->
137+ reify bs (map Right ) $ \ rs ->
138+ k `elem_` ls ++. rs
139139 ]
140140 ]
141141
142142keysExample :: Specification (Either Int Int )
143- keysExample = constrained $ \ k ->
144- [ caseOn k
145- (branch $ \ a -> a `elem_` as)
146- (branch $ \ b -> b `elem_` bs)
147- , reify as (map Left ) $ \ ls ->
148- reify bs (map Right ) $ \ rs ->
149- k `elem_` ls ++. rs
150- ] where as = lit [ 1 .. 10 ]
151- bs = lit [ 11 .. 20 ]
143+ keysExample = constrained $ \ k ->
144+ [ caseOn
145+ k
146+ (branch $ \ a -> a `elem_` as)
147+ (branch $ \ b -> b `elem_` bs)
148+ , reify as (map Left ) $ \ ls ->
149+ reify bs (map Right ) $ \ rs ->
150+ k `elem_` ls ++. rs
151+ ]
152+ where
153+ as = lit [1 .. 10 ]
154+ bs = lit [11 .. 20 ]
0 commit comments