ucsd-progsys/liquidhaskell
Auf GitHub ansehenDocument that specs can depend on arguments of enclosing functions
Open
#2.442 geöffnet am 19. Nov. 2024
documentationgood first issue
Repository-Metriken
- Stars
- (1.306 Stars)
- PR-Merge-Metriken
- (Durchschn. Merge 2T 18h) (12 gemergte PRs in 30 T)
Beschreibung
Today I learned that the meaning of specs of local bindings can depend on arguments of an enclosing function. For instance, in the following function from the test suite, arg0 is available to the spec of bar.
{-@ foo :: x:_ -> y:_ -> {v:Int | v = x + y} @-}
foo :: Int -> Int -> Int
foo arg0 = bar
where
{-@ bar :: x:_ -> {v:Int | v = x + arg0} @-}
bar arg1 = arg0 + arg1
It doesn't work for other things than arguments though, e.g. z is not in scope in the following spec.
{-@ foo :: x:_ -> y:_ -> {v:Int | v = x + y} @-}
foo :: Int -> Int -> Int
foo arg0 = bar
where
z = arg0
{-@ bar :: x:_ -> {v:Int | v = x + z} @-}
bar arg1 = arg0 + arg1
We should document the fact that arguments of enclosing functions are in scope. This is also true for other local bindings. See the comments below.