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❙
❚