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

import real scala://real.omdoc.org/❚
import rules scala://mmt.kwarc.info❚

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

//   A first test case for writing imperative programs as MMT theories. ❚
theory ProgLang : http://cds.omdoc.org/urtheories?CF =
  include ☞real:?Bool❙
  include ?NatRules❙
  include ☞real:?StandardNat❙
  
  print : {a: type} a ⟶ None❘ # print 2❙
  rule rules/cf?Print❙
❚

theory Counter : ?ProgLang =
  counter: nat❘= 0❙
  add: nat ⟶ None❘= [n] counter = counter + n❙
❚  
  
theory Program : ?ProgLang =
  main = print 1❙

  // This one is still experimental.❙
  // main2 =
    var c = new examples?Counter in
    c.add 3;
    print c.add
  ❙
❚