ranjitjhala
commented
4 years ago Thanks for posting this Hafizh! It seems to work fine on my laptop locally
I get the result
**** RESULT: UNSAFE
/Users/rjhala/tmp/Foo.hs:259:32-33: Error: Liquid Type Mismatch
259 | | ok = Just (M r c vs) ^^
Inferred type VV : (IntMeasure.Vector a##xo)
not a subtype of Required type VV : {VV : (IntMeasure.Vector a##xo) | vDim VV == size xs}
In Context xs : {v : [a##xo] | size v >= 0 && len v >= 0}
so let me check and see why the web demo is complaining!
On Tue, May 26, 2020 at 11:57 PM Hafizh Afkar Makmur < notifications@github.com> wrote:
This code http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1590562380_9269.hs fails to compile and gives "Request Failed0" instead. Is there anything wrong with the code?
PS: While I'm at it, I'm only able to do the quickSort assignment because I'm using assume (++). Is it really the intended way?
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/97__;!!Mih3wA!UlRZASK-_Jot1SbUGV-sckF4llc1ijHvPRcJtbFWEcVtY-ty7dvcOute8iFmDj1z$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OER7HVRJ5RRUN2F6Y3RTS2TZANCNFSM4NL24TLA__;!!Mih3wA!UlRZASK-_Jot1SbUGV-sckF4llc1ijHvPRcJtbFWEcVtY-ty7dvcOute8kE1VgO6$ .
hafizhmakmur
This code fails to compile (stuck at "Verifying...") and gives "Request Failed0" instead. Is there anything wrong with the code?
PS: While I'm at it, I'm only able to do the
quickSortassignment because I'm usingassume (++). Is it really the intended way?