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

rule scala://parser.api.mmt.kwarc.info?MMTURILexer❚

theory Terms =
   include ☞/urtheories?Typed❙
   
   formation # {| 1 |} 2 prec -10000❙
   reflect   # ⌜ 1 : 2 ⌝ prec -10000❙
   eval      # ⌞ 1 ⌟ 2   prec -10000❙
   elim      # 1 ^ 2     prec -10000❙
❚

theory LFReflection =
  include ☞/urtheories?LF❙
  include ?Terms❙
❚