Skip to content

Add unfoldings for local bindings outside the simplifier

Motivation

I am working on a Core plugin that is interested in unfoldings. The natural place for such a plugin to run is at the start of the pipeline. However, if we look around at that point, we see:

  • Bindings from other modules have unfoldings.
  • Some bindings from other packages have unfoldings (as we'd expect, depending on INLINEABLE etc.)
  • Local bindings do not have unfoldings.

After some poking around, I think these are actually added by the simplifier (see completeBinding). I'm not really sure why it happens there, but it would be nice to be able to ensure that the unfoldings were present without having to run the whole simplifier, which does many other things too.

Proposal

Move the creation of local unfoldings somewhere else, maybe desugaring?

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information