namespace http://cds.omdoc.org/urtheories❚

import rules scala://substructural.mmt.kwarc.info❚

// This theory is under development.
Its goal is to investigate to what extent substructural languages can be represented in MMT.
This was motivated by a promising initial case study on representing ordered linear logic (done with Jeff Polakow, at LFMTP 2017).❚

//   theory Substructural =
   Sarrow  # 2 - 1 -> 3  prec  -9990❙
   Slambda # [ 1 V2T,… ] 2 prec -10000❙
   Sapply  # 1%w…        prec -10❙

   class # class 1 2  prec 1000❙

   unordered ❙
   leftordered ❙
   rightordered ❙
   
   plain❙
   useall❙
   useonce❙
   linear❙

   rule rules?SArrowTerm❙
   rule rules?SLambdaTerm❙
   rule rules?SApplyTerm❙
   rule rules?SArrowTyping❙
   rule rules?SArrowEquality❙
   rule rules?SArrowBeta❙
❚