Commit fb1c4ef3 authored by Florian Rabe's avatar Florian Rabe

no message

parent adca1557
......@@ -4,8 +4,8 @@ import lfrules scala://lf.mmt.kwarc.info/❚
import stdlit scala://uom.api.mmt.kwarc.info/❚
theory Framework =
include ur:/?PLF❙
include http://gl.mathhub.info/MMT/LFX/Records?LFRecords❙
include `ur:/?PLF❙
include `http://gl.mathhub.info/MMT/LFX/Records?LFRecords❙
theory MathData : ?Framework =
......@@ -67,7 +67,7 @@ theory MathData : ?Framework =
inRight : {a,b} b ⟶ a ∪ b❙
dunion_cases: {a,b,c: type} a∪b ⟶ (a ⟶ c) ⟶ (b ⟶ c) ⟶ c❙
finiteType: type ⟶ type
finiteType: {a} finset a ⟶ type❘# finiteType 2
/T finiteType a must be subtype of a❙
Ring = {'
......@@ -146,7 +146,7 @@ theory Codecs : ur:?PLF =
ProductAsArray: {A,B,e} codec A e ⟶ codec B e ⟶ codec (A * B) e❙
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❙
FiniteTypeAsItself : {A,a} codec A a ⟶ codec (finiteType A) a❙
FiniteTypeAsItself : {A,S:finset A,a} codec A a ⟶ codec (finiteType S) a❙
FinSetAsArray : {A,a} codec A a ⟶ codec (finset A) (db_array a)❙
PolynomialAsSparseArray : {r, e} codec (r.univ) e ⟶ codec (Poly r) (db_array (db_array e))❘# %%prefix 2 1❙
......
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