A "bind" ties a name to a (refined) type.
Liquid-Fixpoint has two grammars for tests, the "Horn format" and the "new format". In the Horn format we write something like
(forall ((x int) (x>0)) ... )
and the above parses to an H.All over H.Bind, see hBindP in Horn/Parse.hs.
The "new format" for the same bind would be
{x: int | x > 0 }
see top-level Parse.hs.
Until today, we got away with simply calling them "bind" because we only deal with the Horn format now, but introducing the "new format" leads to confusion between the two; this commit renames those binds which mean hBind.
A "bind" ties a name to a (refined) type. Liquid-Fixpoint has two grammars for tests, the "Horn format" and the "new format". In the Horn format we write something like
and the above parses to an H.All over H.Bind, see
hBindPinHorn/Parse.hs. The "new format" for the same bind would besee top-level
Parse.hs.Until today, we got away with simply calling them "bind" because we only deal with the Horn format now, but introducing the "new format" leads to confusion between the two; this commit renames those binds which mean hBind.