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

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

theory Informal =
  informal❙
  rule rules?InformalLiterals❙
  rule rules?InformalTyping❙
❚

theory Semiformal =
  include ?Informal❙

  semiformal❙
  rule rules?SemiformalInterpolation❙
  rule rules?SemiformalTerm❙
❚

theory SemiformalInterpolationExample : ?LF =
  include ?Semiformal❙
  
  nat: type❙
  plus : nat ⟶ nat ⟶ nat❘ # 1 + 2❙
  
  test : nat ⟶ nat ⟶ nat ❘ = [x,y] sf"the sum of all number from 1 to ${x+y}":nat❙
  test2 = [x,y] sf"the product of ${x+y:nat} and ${y+x:nat}":nat❙
❚