[Agda] Not Unfolding Local Defs

Wouter Swierstra w.s.swierstra at uu.nl
Thu May 12 08:37:07 CEST 2016


> Is there a way to tell Agda not to unfold these definitions in goals?

Have you tried using the abstract keyword? I seem to remember that it
can be used prevent the definition being unfolded (but I can't seem to
find any documentation).

  Wouter


More information about the Agda mailing list