This module provides utilities for defining simple opaque types for forward declarations. Types are first declared with declare_opaque_type and then later filled in with hydrate_opaque_type once the corresponding non-opaque type has been defined.

def Lake.declareOpaqueType : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lake.hydrateOpaqueType : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.