namespace latin:/❚
import diagops scala://diagops.latin2❚

/T Declare operator constants

   Use an empty meta theory! E.g. if we used LF as a meta theory the notation
   would be parsed as LF-y.
❚
theory LogicDiagramOperatorsSyntax =
  fol_typifier # TYPIFY FOL 1 prec -2000000 ❙
❚

theory LogicDiagramOperatorsSemantics : ur:?LF =
  include ☞http://cds.omdoc.org/urtheories?ModExp ❙
  rule diagops?ComputeFOLTypified ❙
❚

theory LogicDiagramOperators =
  include ?LogicDiagramOperatorsSyntax ❙
  include ?LogicDiagramOperatorsSemantics ❙

  include ☞http://cds.omdoc.org/urtheories?Combinators ❙
❚