namespace latin:/

fixmeta ur:?LF

import rules scala://mmt.kwarc.info


theory Strings =
  string : type
  rule rules/lf?Realize string rules/api/uom?StandardString
  
  concat : string ⟶ string ⟶ string
  rule rules/lf?Realize concat rules/api/uom?StringOperations/Concat
  
  test : string = "test"


theory CTTQE = 
  include ?TypedLogic
  include ?Strings
  include ?SimpleFunctions
  include ?UndefinedTypedTerms

  Quotation: tp# ε
  rule rules/lf?Realize (tm Quotation) rules/api/uom?TermLiteral 
  
  quote #  1  prec -10050

  eval : tm ε ⟶ {a:tp} tm a #  1 % 2  prec -10050  
  
  const: string ⟶ tp ⟶ tm ε# const 1
  var: string ⟶ tp ⟶ tm ε
  application: tm ε ⟶ tm ε ⟶ tm ε# 1 app 2
  abstraction: string ⟶ tp ⟶ tm ε ⟶ tm ε# abs 1 % 2 . 3
  quotation: tm ε ⟶ tm ε# quo 1 
  
  // rule ComputeApply❙


theory Example =
  include ?CTTQE