Variable ==> not in scope

[jessebrennan]

While plugging in examples from the tutorial I got this error

$ liquid tutorial.hs 
LiquidHaskell Version 0.8.2.4, Git revision ec88f568d101bfd35b6254aa7db034164d9c89dd
Copyright 2013-18 Regents of the University of California. All Rights Reserved.


**** DONE:  annotate ***********************************************************
 

**** RESULT: ERROR *************************************************************


Invalid Source


 /home/jesse/projects/lh-tutorial/tutorial.hs:11:20-22: Error: GHC Error
  
 11 | ex4 a b = (a && b) ==> a
                         ^^^
  
     
         Variable not in scope: (==>) :: Bool -> Bool -> t

The contents of tutorial.hs:

{-@ type FALSE = {v:Bool | not v} @-}
{-@ type TRUE = {v:Bool | v} @-}

{-@ ex1 :: Bool -> TRUE @-}
ex1 b = b || not b

{-@ ex2 :: Bool -> FALSE @-}
ex2 b = b && not b

{-@ ex4 :: Bool -> Bool -> TRUE @-}
ex4 a b = (a && b) ==> a

{-@ ex5 :: Bool -> TRUE @-}
ex5 b = b || not b

ALSO

$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 8.0.2

I'm new to this, not really sure what is going wrong or what other info I can provide. What am I doing wrong? Thanks

[ranjitjhala]

Hi, this is because there are some “hidden” definitions that are in the lhs file that are not rendered in the html or pdf. You can grab those definitions from the repo. (Apologies about this — it’s a design flaw in the tutuorial that I haven’t gotten around to fixing yet!)

…

On Mon, Jul 16, 2018 at 11:14 PM jessebrennan ***@***.***> wrote: While plugging in examples from the tutorial I got this error $ liquid tutorial.hs LiquidHaskell Version 0.8.2.4, Git revision ec88f56 Copyright 2013-18 Regents of the University of California. All Rights Reserved. **** DONE: annotate *********************************************************** **** RESULT: ERROR ************************************************************* Invalid Source /home/jesse/projects/lh-tutorial/tutorial.hs:11:20-22: Error: GHC Error 11 | ex4 a b = (a && b) ==> a ^^^ Variable not in scope: (==>) :: Bool -> Bool -> t The contents of tutorial.hs: {-@ type FALSE = {v:Bool | not v} @-} {-@ type TRUE = {v:Bool | v} @-} {-@ ex1 :: Bool -> TRUE @-} ex1 b = b || not b {-@ ex2 :: Bool -> FALSE @-} ex2 b = b && not b {-@ ex4 :: Bool -> Bool -> TRUE @-} ex4 a b = (a && b) ==> a {-@ ex5 :: Bool -> TRUE @-} ex5 b = b || not b ALSO $ ghc --version The Glorious Glasgow Haskell Compilation System, version 8.0.2 I'm new to this, not really sure what is going wrong or what other info I can provide. What am I doing wrong? Thanks — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#1345>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABkuOAASAeVBFVwHdpbH4aasddvUyJDrks5uHYC4gaJpZM4VSPb1> .

[ranjitjhala]

Each chapter in the tutorial is generated from the corresponding LHs file that is in the tutorial repo: you can get all the definitions from that file...

…

On Tue, Jul 17, 2018 at 7:21 AM Ranjit Jhala ***@***.***> wrote: Hi, this is because there are some “hidden” definitions that are in the lhs file that are not rendered in the html or pdf. You can grab those definitions from the repo. (Apologies about this — it’s a design flaw in the tutuorial that I haven’t gotten around to fixing yet!) On Mon, Jul 16, 2018 at 11:14 PM jessebrennan ***@***.***> wrote: > While plugging in examples from the tutorial I got this error > > $ liquid tutorial.hs > LiquidHaskell Version 0.8.2.4, Git revision ec88f56 > Copyright 2013-18 Regents of the University of California. All Rights Reserved. > > > **** DONE: annotate *********************************************************** > > > **** RESULT: ERROR ************************************************************* > > > Invalid Source > > > /home/jesse/projects/lh-tutorial/tutorial.hs:11:20-22: Error: GHC Error > > 11 | ex4 a b = (a && b) ==> a > ^^^ > > > Variable not in scope: (==>) :: Bool -> Bool -> t > > > The contents of tutorial.hs: > > {-@ type FALSE = {v:Bool | not v} @-} > {-@ type TRUE = {v:Bool | v} @-} > > {-@ ex1 :: Bool -> TRUE @-} > ex1 b = b || not b > > {-@ ex2 :: Bool -> FALSE @-} > ex2 b = b && not b > > {-@ ex4 :: Bool -> Bool -> TRUE @-} > ex4 a b = (a && b) ==> a > > {-@ ex5 :: Bool -> TRUE @-} > ex5 b = b || not b > > > ALSO > > $ ghc --version > The Glorious Glasgow Haskell Compilation System, version 8.0.2 > > I'm new to this, not really sure what is going wrong or what other info I > can provide. What am I doing wrong? Thanks > > — > You are receiving this because you are subscribed to this thread. > Reply to this email directly, view it on GitHub > <#1345>, or mute the > thread > <https://github.com/notifications/unsubscribe-auth/ABkuOAASAeVBFVwHdpbH4aasddvUyJDrks5uHYC4gaJpZM4VSPb1> > . >

[jessebrennan]

I wouldn't mind doing a PR to clear up the docs here. As for the approach, do you think a better warning is sufficient or it would be worth while to add all of the 'hidden' bits to the docs? I haven't gotten very far into the tutorial (as you can tell) so I'm not completely sure what that would entail.

[ranjitjhala]

Hmm, good question -- are you reading the docs online or on the PDF?

The easiest would be to just remove the \begin{comment} and \end{comment} lines, e.g.

• https://github.com/ucsd-progsys/liquidhaskell-tutorial/blob/master/src/02-logic.lhs#L5
• https://github.com/ucsd-progsys/liquidhaskell-tutorial/blob/master/src/02-logic.lhs#L34

so everything gets rendered...

[jessebrennan]

I was reading online. As a side note, the online notes weren't working for me at home so I was using the PDF there.

[jessebrennan]

The easiest would be to just remove the \begin{comment} and \end{comment} lines, e.g.

That makes sense to me. I would add some context / instructions too. Just give me the OK.

[jessebrennan]

@ranjitjhala let me know if a PR to fix this would be appreciated.

[ranjitjhala]

Yes it would be most appreciated!

…

On Wed, Jul 18, 2018 at 5:33 PM jessebrennan ***@***.***> wrote: @ranjitjhala <https://github.com/ranjitjhala> let me know if a PR to fix this would be appreciated. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#1345 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABkuOHKWOqbZDN9O6lrq7ofYWEXVHzJPks5uH9PSgaJpZM4VSPb1> .