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

import real scala://real.omdoc.org/❚

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

theory NatLiterals : http://cds.omdoc.org/urtheories?LF =
  include ?NatRules❙
  include ☞real:?Bool❙
  include ☞real:?StandardNat❙
  
  // this only type-checks because ⊦ 1+1 = 2 unifies with ⊦ true ❙
  test  : ⊦ 1+1 = 2❘ = trueI❙
❚
  
theory IntLiterals : http://cds.omdoc.org/urtheories?LF =
  include ?IntRules❙ // this should include NatRules, but the last test only works with the rule IntRules?succ_invert/Solve❙
  include ☞real:?Bool❙
  include ☞real:?StandardInt❙
  test  : ⊦ 1-3 = -2 ❘ = trueI❙
❚

theory Vectors : http://cds.omdoc.org/urtheories?LF =
  include ?NatLiterals❙

  a     : type❙
  c     : a❙
  
  a_equal : a ⟶ a ⟶ type❘ # 1 = 2 ❘role Eq❙

  vec   : nat ⟶ type ❘ # vec 1 prec 5❙
  empty : vec 0 ❘ # ∅ ❙
  cons  : {n} vec n ⟶ a ⟶ vec n' ❘ # 2 , 3❙

  vec_equal : {n} vec n ⟶ vec n ⟶ type❘ # 2 == 3❘role Eq❙
  
  append      : {m,n} vec m ⟶ vec n ⟶ vec (m + n) ❘ # 3 @ 4❙
  // this only type-checks because vec n+0 and vec n are recognized as equal ❙
  appendempty : {n, v: vec n} v @ ∅ == v❙
  // this only type-checks because vec m + (n') and vec (m + n)' are recognized as being equal ❙
  appendcons  : {m,n, x, v: vec m, w: vec n} v @ (w,x) == (v @ w, x)❙
  
  last : {n} vec n' ⟶ a ❘ # last 2❙
  lastcons : {n, x, v: vec n} last (v,x) = x ❘role Simplify❙
  
  // this only type-checks because vec 3 and vec 0''' are recognized as equal ❙
  test1 : vec 3 ❘ = ∅,c,c,c❙
  // this only type-checks because vec 6 and vec (3+3) are recognized as equal ❙
  test2 : vec 6 ❘ = test1 @ test1 ❙
  // this only type-checks because vec n' unifies with vec 3❙
  test3 : a ❘= last test1❙
❚