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

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

theory Nat : ../urtheories?LF =
  nat : type❙
  zero: nat❙
  succ: nat⟶nat ❘# 1 ' prec 10❙
  
  rule rules/lf?Realize nat  rules/api/uom?StandardNat❙
  rule rules/lf?Realize zero rules/api/uom?Arithmetic/Zero❙
  rule rules/lf?Realize succ rules/api/uom?Arithmetic/Succ❙
❚

theory Bool : ../urtheories?LF =
  bool: type❙
  proof: bool ⟶ type ❘# ⊦ 1 prec -5❙
❚

theory DHOL : ../urtheories?LF  =
  include ?Nat❙
  include ?Bool❙
  rule rules/lf?ShallowPolymorphism❙
  equal : {a:type} a ⟶ a ⟶ bool ❘# 2 = 3 prec 5❙
❚

theory Double : ?DHOL =
  double : nat ⟶ nat❙
  double_zero: ⊦ double 0 = 0❙
  double_succ: {x} ⊦ double(x') = (double x)''❙
❚