Facundo Domínguez

I see. Despite the fact that GHC erases newtypes, it looks like it should be possible to generate those constants with the Bag occurrences found in the specs. I'm not...

I think LF already allows to do it, except that it has no predefined sort for optional values (like `Maybe a`).

It is possible to define ``` define empty = (Map_default Nothing) define insert x y m = (Map_store m x (Just y)) define lookup x m = (Map_select m x)...

> Regarding CVC5, I don't believe it supports any operations on Array beyond const, select and store — map is indeed needed to implement unions, intersections, etc. The situation here...

Even if we assume we have `map`, implementing `union` would be some challenge. SMTLIB requires monomorphic sorts for functions. So in ``` (define-fun union_p2p ((oa0 (Option a)) (oa1 (Option a)))...

~This doesn't address the restriction of monomorphic sorts, but I just found that `map` can be approximated in CVC5 with `as-array`.~ The following snippet was generated with ai: ```lisp (set-logic...

Oh, it is me who is hallucinating. I thought I have tested the script well. 😞 Please, excuse me for the noise.

A more radical approach here would be to ditch arrays, and instead use plain functions to represent containers like sets and maps. There are two motivations to stay away from...

There is a type alias `TT` defined in [src/GHC/Types_LHAssumptions.hs](https://github.com/ucsd-progsys/liquidhaskell/blob/5536a9ecd2bacb2d154b307351471401afb2835a/src/GHC/Types_LHAssumptions.hs#L52). Removing the type alias fixes the error. This ticket seems to be about a bad error message then. I would expect...

Using this definition ```Haskell infixl 3 ? (?) :: a -> b -> a (?) a _ = a ``` instead of the one in ProofCombinators, limits the amount of...