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