Documentation

ProofWidgets.Component.PenroseDiagram

Instances For
    Equations

    Displays the given diagram using Penrose. The website contains explanations of how to write domain (dsl), style (sty), and substance (sub) programs.

    The diagram may also contain embedded HTML trees which are specified in embeds. Each embed is HTML together with the name of an object x in the substance program. The object x can be of any type but must be assigned an x.textBox : Rectangle field in the style program. This rectangle will be replaced with the HTML tree. Its dimensions will be overridden in the style program to match those of the HTML node.

    The following additional constants are prepended to the style program:

    theme {
      color foreground
      color tooltipBackground
      color tooltipForeground
      color tooltipBorder
    }
    

    and can be accessed as, for example, theme.foreground in the provided sty in order to match the editor theme.

    Instances For

      DiagramBuilderM #

      Instances For
        @[reducible, inline]

        A monad to easily build Penrose diagrams in.

        Equations
        Instances For

          Assemble the diagram using the provided domain and style programs.

          none is returned iff nothing was added to the diagram.

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

            Add an object nm of Penrose type tp, labelled by h, to the substance program.

            Equations
            Instances For

              Add an object of Penrose type tp, corresponding to (and labelled by) the expression e, to the substance program. Return its Penrose name.

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

                Add an instruction i to the substance program.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • x.run = StateT.run' x { sub := "", embeds := Std.HashMap.empty }
                  Instances For
                    @[reducible, inline]

                    Abbreviation for backwards-compatibility.

                    Equations
                    Instances For
                      @[reducible, inline]

                      Abbreviation for backwards-compatibility.

                      Equations
                      Instances For