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❙
❚