Merge pull request #1425 from ucsd-progsys/T1420

add smallstep notes
ucsd-progsys · Mar 17, 2019 · 8c121ce · 8c121ce
2 parents e557f2f + 6b60810
commit 8c121ce
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/include/Language/Haskell/Liquid/Equational.hs b/include/Language/Haskell/Liquid/Equational.hs
@@ -42,7 +42,8 @@ _ `eq` x = x
 
 infixl 3 ?
 
-(?) :: a -> Proof -> a 
+{-@ (?) :: forall a b <pa :: a -> Bool, pb :: b -> Bool>. a<pa> -> b<pb> -> a<pa> @-}
+(?) :: a -> b -> a 
 x ? _ = x 
 {-# INLINE (?)   #-} 
 
@@ -51,4 +52,4 @@ x ? _ = x
 -------------------------------------------------------------------------------
 
 withTheorem :: a -> Proof -> a 
-withTheorem z _ = z 
+withTheorem z _ = z