LF meeting today was pretty interesting. Talked about the definitions (both strict and %abbrev style) at the term and type level and how they might interact with the module system.