Facundo Domínguez

I'm guessing that resolving this would require adding this example to the [section on termination metrics](https://ucsd-progsys.github.io/liquidhaskell/specifications/#termination-metrics) of the website.

> Will leave this open till I can get around to fixing this... What would the fix be? Replacing the measures with reflected functions perhaps?

Any further thoughts on how to address this issue?

At the moment it is possible to exclude specs coming from some particular package `--exclude-automatic-assumptions-for=PACKAGE`. But excluding specs from the `liquidhaskell` module would likely exclude too much. A similar mechanism...

Probably resolving #2126 will make this more approachable.

Hello @MrPowers. We could consider merging contributions related to Spark Connect. It is unclear to me what support is needed on the sparkle side, but feel free to open issues...

These functions seem to be defined in [liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs](https://github.com/ucsd-progsys/liquidhaskell/blob/45cac37fe6fd79ca68a0469bd29cef018ee36260/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs). Update: the various define annotations have been spread in the LHAssumption modules now. `div` and `mod` annotations are in `src/GHC/Real_LHAssumptions.hs` now.

It might have no effect in this example. I know that it enables at least `--exactdc` and `--higherorder`.

> eg if you have function types in the data definition.. IIRC, functions are replaced with integers to describe higher order functions to the SMT solver. Could we hope to...

Given the work I'm doing at the moment, my biased preference is that names are kept the same as used in the PDF documents for older eras.