mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-10 15:16:54 +03:00
Adjust ST makeAndIncrement example type
`Int -> ST m Int []` is incompatible with previous examples which use `Integer`. When using `Int` in the type of `makeAndIncrement`, you'll get something like this: ``` - + Errors (1) `-- ST.idr line 20 col 27: When checking right hand side of makeAndIncrement with expected type STrans m Int [] (\result => []) When checking an application of function Control.ST.>>=: Error in state transition: Operation has preconditions: [x ::: State Integer] States here are: [var ::: State Int] Operation has postconditions: \result => [x ::: State Integer] Required result states here are: st2_fn ```
This commit is contained in:
parent
4064dcf1c8
commit
4c95e68f8f
@ -594,7 +594,7 @@ That is, ``increment`` begins and ends with ``x`` in state ``State Integer``.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
makeAndIncrement : Int -> ST m Int []
|
||||
makeAndIncrement : Integer -> ST m Integer []
|
||||
|
||||
That is, ``makeAndIncrement`` begins and ends with no resources.
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user