Commit abaebe54 authored by Florian Rabe's avatar Florian Rabe

no message

parent 74af6271
......@@ -19,7 +19,7 @@ theory Example : ?SchemaLang =
meta ?Codecs?codec IntIdent❘
orthogonal: bool
orthogonal: bool
meta ?Codecs?codec BoolIdent❘
......
......@@ -3,7 +3,12 @@ namespace http://data.mathhub.info/schemas❚
import lfrules scala://lf.mmt.kwarc.info/❚
import stdlit scala://uom.api.mmt.kwarc.info/❚
theory MathData : ur:/?PLF =
theory Framework =
include ur:/?PLF❙
include http://gl.mathhub.info/MMT/LFX/Records?LFRecords❙
theory MathData : ?Framework =
bool : type❙
rule lfrules?Realize bool stdlit?StandardBool❙
......@@ -19,9 +24,9 @@ theory MathData : ur:/?PLF =
geq : int ⟶ int ⟶ bool❘# 1 ≥ 2❙
string: type❙
concat : string ⟶ string ⟶ string ❘# 1 @ 2❙
strconcat : string ⟶ string ⟶ string ❘# 1 @ 2❙
rule lfrules?Realize string stdlit?StandardString❙
rule lfrules?Realize concat stdlit?StringOperations/Concat❙
rule lfrules?Realize strconcat stdlit?StringOperations/Concat❙
uuid: type❙
rule lfrules?Realize uuid stdlit?UUIDLiteral❙
......@@ -50,17 +55,29 @@ theory MathData : ur:/?PLF =
left : {a,b} product a b ⟶ a ❘# 3 _1❙
right : {a,b} product a b ⟶ b❘# 3 _2❙
Ring: type❙
ring: {a: type, plus: a ⟶ a ⟶ a, minus: a ⟶ a, zero: a, times: a ⟶ a ⟶ a, one: a} Ring❙
univ: Ring ⟶ type❙
IntegerRing: Ring❘= ring int plus ([x] 0-x) 0 times 1❙
Ring = {'
univ: type,
plus: univ ⟶ univ ⟶ univ,
minus: univ ⟶ univ,
zero: univ,
times: univ ⟶ univ ⟶ univ,
one: univ
'}❙
IntegerRing: Ring❘= ['
univ := int,
plus := plus,
minus := [x] 0-x,
zero := 0,
times := times,
one := 1
']❙
var: type ❘ = string❙
PolynomialRing : Ring ⟶ Ring❘# PolyRing 1 prec 10❙
Polynomial : Ring ⟶ type❘ = [r] univ (PolyRing r)❘ # Poly 1 prec 10❙
polynomial : {r} var ⟶ list (univ r) ⟶ Poly r❙
coeffs : {r} Poly r ⟶ list (univ r)
Polynomial : Ring ⟶ type❘ = [r] (PolyRing r).univ❘ # Poly 1 prec 10❙
polynomial : {r} var ⟶ list r.univ ⟶ Poly r❙
coeffs : {r: Ring} Poly r ⟶ list r.univ
degree : {r} Poly r ⟶ int❙
......@@ -112,8 +129,8 @@ theory Codecs : ur:?PLF =
MatrixAsArray : {A,a,m,n} codec A a ⟶ codec (matrix A m n) (db_array (db_array a))❘
= [A,a,m,n,C] VectorAsArray n (VectorAsArray m C)❘# MatrixAsArray 5❙
PolynomialAsSparseArray : {r, e} codec (univ r) e ⟶ codec (Poly r) (db_array (db_array e))❘# %%prefix 2
PolynomialAsDenseArray : {r, e} codec (univ r) e ⟶ codec (Poly r) (db_array e)❘# %%prefix 2
PolynomialAsSparseArray : {r, e} codec (r.univ) e ⟶ codec (Poly r) (db_array (db_array e))❘# %%prefix 2 1
PolynomialAsDenseArray : {r, e} codec (r.univ) e ⟶ codec (Poly r) (db_array e)❘# %%prefix 2 1
theory CommutingOps : ur:?PLF =
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment