Documentation

StrataDDM.BuiltinDialects.BuiltinM

source
@[reducible, inline]
abbrev StrataDDM.Elab.BuiltinM (α : Type) :
Type
Equations
Instances For
    source
    def StrataDDM.Elab.BuiltinM.create! (name : DialectName) (dialects : Array Dialect) (act : BuiltinM Unit) :
    Dialect
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def StrataDDM.Elab.BuiltinM.addDecl (decl : Decl) :
      BuiltinM Unit
      Equations
      Instances For
        source
        def StrataDDM.Elab.declareCat (cat : QualifiedIdent) (argNames : Array String := #[]) :
        BuiltinM Unit
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def StrataDDM.Elab.declareAtomicCat (cat : QualifiedIdent) :
          BuiltinM Unit
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def StrataDDM.Elab.declareOp (decl : OpDecl) :
            BuiltinM Unit
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def StrataDDM.Elab.declareMetadata (decl : MetadataDecl) :
              BuiltinM Unit
              Equations
              Instances For