namespace latin:/❚

fixmeta latin:/?SFOLEQND❚

import rules scala://lf.mmt.kwarc.info❚
import uom scala://uom.api.mmt.kwarc.info❚

theory Nat =
  nat   : tp❙
  Nat = tm nat❘# ℕ❙
  zero  : ℕ❙
  succ  : ℕ ⟶ ℕ❘ # 1 ' prec 20❙
  
  rule rules?Realize ℕ uom?StandardNat❙
  rule rules?Realize zero uom?Arithmetic/Zero❙
  rule rules?Realize succ uom?Arithmetic/Succ❙
❚