Mathlingua

Mathlingua logo

Mathlingua is a language designed to record, share, and communicate mathematical knowledge with the goal to be more precise and easier to read and write than mathematics written in a natural languages.

The main usage of Mathlingua is for the development of mathlore.org, a community developed collection of all mathematics described in the Mathlingua language.


Mathlingua is a language specially designed to create mathlore.org, a collection of mathematical knowledge with the goal to make it easier to learn, communicate, and understand mathematics. In particular to: * remove ambiguity * illustrate the relationship between mathematical concepts * highlight aspects of definitions and theorems that are easy to overlook * automatically identify some errors in definitions and theorems

It is created to address the unique needs for recording mathematical knowledge, that include but are not limited to:

The Need for a Recording Mathematics

There are many examples in mathematics of concepts being rediscovered. This could be from the fact that it is often times difficult to find what has already been discovered. This is compounded by the observation that different authors can use very different nomenclature and notation for the same concepts.

Further, as more and more mathematics is discovered, it is becoming harder and harder for any individual to follow everything new. This is especially difficult since many discoveries may be in journals that are hard to search and require subscriptions, and thus are not accessible to most.

As a result, a standard repository of all mathematics in a clear, consistent format is needed to help this and future generations discover and record mathematics.

Existing Math Collections

Existing collections of mathematical knowledge typically fall into two categories. First are books, articles, journals, encyclopedias, etc. while the second are collections written in theorem proving languages such as Lean, Coq, Mizar, etc.

For the first category, different math concepts can be spread across different books or other resources. Even for encyclopedias, nomenclature and notation can vary across the encyclopedia.

Next, these resources are written in natural language, and are thus difficult for computers to search and understand. That is, it is not easy to make computer search capabilities to search math books, journals, and encyclopedias and find, for example, all theorems that describe when a function is measurable.

Further, mathematics written in natural language can be imprecise and difficult to read because statements can rely on context or conventions for information. For example, a theorem might say for all \(x\) and \(y\) there exists an \(n\) such that \(x*n > y\), where it is up to the reader to infer, based on convention and the fact that the theorem is in a real analysis book, that \(x\) and \(y\) refer to real numbers and \(n\) an integer.

Last, mathematics written in natural language do not have any automated checking of any aspects of the statements. In particular, a statement could have a typo in a symbol name, thus using a name that is not defined anywhere or refer to a definition that doesn’t exist, and it is up to manual review to catch those mistakes.

Getting Started

Mathlore is the site that hosts the community grown collection of mathematical knowledge encoded in the Mathlingua language. You can access it at mathlore.org. Contributions to Mathlore are welcome from everyone.

To get started first fork the repository. Next, download the latest release of the Mathlingua command line tool from the releases page, rename it to mlg, and ensure it is in your PATH.

Last, you can use whatever editor you like to edit Mathlingua code. However, if you use Visual Studio Code you can install the Mathlingua Language Support extension that provides syntax highlighting, autocompletion, and error diagnostics provided by mlg.

Mathlingua files have the .math extension and the mathlingua-language-support extension is designed to analyze any files with the .math extension.

The Mathlingua Tooling

mlg is the Mathlingua command line tools used to interact with collections of Mathlingua documents. It uses the format mlg <command> where <command> is an action to perform:

About the Author

Mathlingua is designed and implemented by Dominic Kramer.

Dominic has a PhD in mathematics from Iowa State University, has over ten years of extensive software design and engineering experience in top companies such as Google, Databricks, and Boeing, and has spent much time, both professionally and personally, working in the area of computer and natural language design and implementation.

Dominic’s interests focus on the intersection of mathematics and languages and includes all aspects of language design and usage ranging from traditional parser design and lambda calculus (ranging from simple to dependent type theory), all of the way to deep learning and large language models.

Dominic is particularly interested in how the design of a language’s syntax and semantics shapes how concepts or applications can or cannot be easily expressed or implemented in that language.

Any questions, comments, or feedback is greatly appreciated, and you can post feedback as an issue in the Mathlingua GitHub repo or via email at DominicKramer@gmail.com.

The Language

Formulation Forms

Names

x
x?
"a b"

Functions

f(x, y)

Infix Operators

x * y

Prefix Operator

+x

Suffix Operator

x!

Tuples

(x, y)

Conditional Sets

TODO: Update this

{x : s(x)... | p(x)}
{x : s(x)...}
{f(x, y) : s(x, y)... | p(x, y)}
{f(x, y) : s(x, y)...}

Functional Literal

x |-> f(x)
(x, y) |-> f(x, y)

Conditional Set Id Form

TODO: update this

[x]{x : s(x)... | p(x)}
[x]{x : s(x)}
[x]{x | p(x)}

Colon Equals Form

X := (a, b)
f(x) := y
f(x) := (a, b)

Formulation Expressions

Function Expression

f(x + y, z)
(f + g)(x)

Function Literals

x |-> x + 1
(x, y) |-> x + y

Tuples

(x + y, z)

Groupings

(x + y)

Invisible Groupings

TODO: update this to be (..)

(.x + y.)

Substitution

TODO: add this

(x + y)[|x := 0; y := a|]
(x + y * z)[|x:= 1; ? := 0|]
(x, y)[| x := 0 |]

Encoding Cast

TODO: add this

{:x:}

Symbols

TODO: add this

$x
$x, $y
[$x] from [a, b]
[$x, $y] from [a, b]
$x...
[$x...] from [a...]

Conditional Set Expression

TODO: update this to use the second |

[x]{(x, x+1) : x is \real | x > 0}
[x]{(x, x+1) : x is \real}
[x, y]{x + y : x, y is \real | x > 0 \.and./ y > 0}

Command Expressions

TODO: update to use second | TODO: update this to not support @

\function:on{A}:to{B}
\a.b.c{x, y}
\a.b.c(x, y)
\a.b.c[x, y]{x + y}
\a.b.c[x, y]{x + y : x, y is \real | x > 0 \.and./ y < 0}

Prefix Operator

-x

Postfix Operator

x!

Infix Operator

x + y

Is Expression

x is \y
x is \y & \z

Equality

x = y
x != y

Extends Expression

TODO: verify if this is actually needed. Update: This is not needed because \\abstract is used instead.

x extends \y

As Expression

x as \:y
x as (a, b, c)

The as operator is used to cast a symbol to another type or another form. The x as (a, b, c) form is used to cast to another form.

When processing x as <form> the type of x is used to determine if it has a view as the specified form. If so, that description is used to convert to the form. Otherwise, if x is a tuple and
is a tuple containing a subset of the items from x, then the cast is that tuple of the subset of the items (where

doesn’t need to have elements in the same order as x). Otherwise, the cast fails (for opaque symbols, functions, or sets).

When processing x as \:<type> the type of x is used to determine if x can be cast as the specified type.

Note: The as operator can be used twice to convert to another type so that the form can also be changed.

x as \:function as [a,b]{(a,b) : s(a, b)...}

Implicit Conversions

A tuple will automatically cast to a tuple with fewer elements. That is, if X := (a, b, c) then one can write X is \something where \something expects a tuple of the form (x, y).

Functions, opaque symbols, and sets do not have implicit conversions.

The consequence of this is that it is possible to write something like:

R := (X, +, *, 0, 1) is \commutative.ring
R is \commutative.ring.with.identity

The \commutative.ring.with.identity expects to be of the form (X, +, *, 0, 1) but \commutative.ring only needs to be of the form (X, +, *, 0). This is ok because the (X, +, *, 0, 1) is cast as (X, +, *, 0) and the \commutative.ring definition only sets the types of X, +, *, and 0.

Ordinal Id Expression

TODO: ADD THIS

x{i := 1...}
x{i := 1...n}
x{(i,j) := (1,1)...}
x{(i,j) := (1,1)...(m,n)}

Ordinal Call Expression

x{i}
x{1}

Ordinal Slice Expression

TODO: ADD THIS

x{1...n}
x{2...n}
x{1...(n-1)}
x{2...(n-1)}

Chain Expression

(x + y).z.a.b

Select From Builtin

\\select{statement|specification}:from{x}

Signatures

A signature is a type without any types for the inputs specified.

TODO: update this to use symbols

\:a.b.c:d:e

Types

\:a.b.c:x{\x & \:a & \:b, \:c}:y{\:d}
\:continuous.function:on{\:set}:to{\:set}
\:continuous.function:on{?}:to{?}
(\:set & \:group) \:to:/ \:set
\:set \:to:/ \:set

Type Builtin

TODO: Remove this and instead have it be just \\type so one can write T is \\type to signify an argument is a type. Also, double check that this is approach makes sense.

\\type{\:set & \:group & \:ring}

Formulation Builtin

TODO: Remove this. Since sets have the form {x : y | z} only \\expression, \\statement and \\specification are needed. (one doesn’t need to OR them).

\\formulation{expression | statement}

Boolean Builtin

\\boolean

Boolean Value Builtin

TODO: Remove this and instead for a statement P saying if: P means if P is true.

\\true
\\false

Type-of Builtin

TODO: Determine if this is needed because of dependent typing

\\type:of{x}

Abstract Builtin

TODO: Add this

\\abstract

Map Builtin

TODO: REMOVE THIS

\\map{x[i]}:to{x[i] + 1}

Map Else Builtin

TODO: REMOVE THIS

\\map{x[i[k]]}:to{x[i[k]] + 1}:else{0}

Definition Of Builtins

\\definition:of{f}
\\definition:of{f}:satisfies{\:continuous.function:on:to}
\\definition:of{f}:satisfies{\:continuous.function:on{A}:to{B}}
\\definition:of{f}:satisfies{\:continuous.function:on:to::(some.label)}
\\definition:of{f}:satisfies{\:continuous.function:on{A}:to{B}::(some.label)}
\\definition:of{A \subset/ B}:satisfies{\:some.thing}
\\definition:of{A \subset/ B}:satisfies{\:some.thing::(some.label)}

Colon Equals Expression

f(x) := x + 1

Colon Arrow Expression

x + y :=> x

Colon Dash Arrow Expression

x [.in.]: y :-> x; y

Enclosed Non-command Operator

TODO: update this to only use [. .] form and not {. .} form

[.x.]:
[.x.]
:[.x.]

Non-enclosed Non-command Operator

*
++
:+
+:

Infix Command Expression

TODO: update this to use the form .x./ and not {x}/ or [x]/

\.function:on{A}:to{B}./

Ids

Command Id

TODO: update this to no longer use @

\function:on{A}:to{B}
\function:on{A}:to[x,y]{f(x,y)}@{x}
\function:on{A}:to[x,y]{f(x,y)}@d{x}

Prefix Operator Id

-x

Postfix Operator Id

x!

Infix Operator Id

x + y

Infix Command Operator Id

TODO: update this to only allow .x./ form and not {x}/ or [x]/

A \.subset./ B

Variadic

TODO: update this to include symbols

x...
x[i...]
x[i...n]
x[i[j...n]]
(x[i[j...n]], y[i[j...n]])
f(x...)
f(x...)...
(x...)
(f(x...)...)
X... := (a, b, c)...
X... := {x | ...}...
X... := {f(x) | ...}...
x... := a...
x... is \a
x... satisfies \a
x... extends \a

TODO: specify what x... = y... means. In particular, (a, b, c) = (x, y, z) defaults to a = x and b = y and c = z.

TODO: Specify that (x...) := (a, b, c) has (x...) interpreted as a tuple and it is different from x... := a... which assigns each on the left to each on the right.

TODO: specify that in f(x...) or \sin(x...) (i.e. where parens are used) the (x...) is the same as ((x...)) where (x...) is interpreted as a tuple. On the other hand, in curly parens such as \f{x...} the x... is interpreted as a variable number of parameters and not a tuple.

:=: expression

TODO: add this

f(x...) :=: f((x...))
f(x, y) :=: f((x, y))
f(x, (y, z)) :=: f((x, y, z))
f(x, y, z) :=: f(x, (y, z))
f(x...) :=: f((x...)) := y

Structural Language

Overview

Clause ::= <Text>
         | <Formulation>
         | <Spec>
         | all:
         | not:
         | anyOf:
         | oneOf:
         | equivalently:
         | exists:
         | existsUnique:
         | forAll:
         | if:
         | iff:
         | when:
         | piecewise:
         | declare:
         | asserting:

Clauses

equivalently: <Clause>+
allOf: <Clause>+
anyOf: <Clause>+
oneOf: <Clause>+
not: <Clause>
exists: <Target>+
using?: <Target>+
where?: <Spec>+
suchThat: <Clause>+
existsUnique: <Target>+
using?: <Target>+
where?: <Spec>+
suchThat: <Clause>+
forAll: <Target>+ 
using?: <Target>+
where?: <Spec>+
suchThat?: <Clause>+
then: <Clause>+
if: <Clause>+
then: <Clause>+
iff: <Clause>+
then: <Clause>+
when: <Spec>
then: <Spec>
piecewise:
if: <Clause>+
then: <Clause>+
elseIf?: <Clause>+
then?: <Clause>+
else?: <Clause>+
declare: <Target>
using?: <Target>+
where?: <Spec>+
suchThat?: <Clause>+
then: <Clause>+

TODO: Add this

asserting: 'a == b'
by?/because?: <ProofItem>+
then: <Spec+>

Inductively

inductively:
oneOf: <InducivelyCase>+

InductivelyCase:

case: <... := ...>
using?: <Target>+

Matching

matching: <Target>
as?: <Type>
against: <MatchingCase>+

MatchingCase:

case: <... := ...>
using?: <Target>+
then: <Clause>

Definitions

TODO: determine if this is needed

Captures: <Formulation>+
Justified?: <JustifiedKind>+
Documented?: <DocumentedKind>+
References?: <Text>+
Writing?: <WritingTextItem>+
Id?: <IdTextItem>

TODO: update this to use specifies: and expresses:

Defines: <Target>
using?: <Target>+
when?: <Spec>+
suchThat?: <Clause>+
means?/equivalentTo: <Spec>+
specifies?: <Spec>+
expresses?: <Clause>+
Provides?: <ProvidesKind>+
Justified?: <JustifiedKind>+
Documented?: <DocumentedKind>+
References?: <Text>+
Aliases?: <Alias>+
Writing?: <WritingTextItem>+
Id?: <IdTextItem>

TODO: update this to use specifies: and satisfies:

Describes: <Target>
using?: <Target>+
when?: <Spec>+
suchThat?: <Clause>+
extends?/equivalentTo: <Spec>+
specifies?: <Spec>+
satisfies?: <Clause>+
Provides?: <ProvidesKind>+
Justified?: <JustifiedKind>+
Documented?: <DocumentedKind>+
References?: <Text>+
Aliases?: <Alias>+
Writing?: <WritingTextItem>+
Id?: <IdTextItem>

TODO: update this to use specifies: and at lease one of specifies: or that: must be specified.

States:
using?: <Target>+
when?: <Spec>+
suchThat?: <Clause>+
specifies?: <Spec>+
that?: <Clause>+
Justified?: <JustifiedKind>+
Documented?: <DocumentedKind>+
References?: <Text>+
Aliases?: <Alias>+
Writing?: <WritingTextItem>+
Id?: <IdTextItem>

Results

Axiom:
given?: <Target>+
declaring?: <Target>+
using?: <Target>+
where?: <Spec>+
suchThat?: <Clause>+
if?: <Clause>+
iff?: <Clause>+
then: <Clause>+
Documented?: <DocumentedKind>+
References?: <Text>+
Aliases?: <Alias>+
Writing?: <WritingTextItem>+
Id?: <IdTextItem>
Conjecture:
given?: <Target>+
declaring?: <Target>+
using?: <Target>+
where?: <Spec>+
suchThat?: <Clause>+
if?: <Clause>+
iff?: <Clause>+
then: <Clause>+
Documented?: <DocumentedKind>+
References?: <Text>+
Aliases?: <Alias>+
Writing?: <WritingTextItem>+
Id?: <IdTextItem>
Corollary:
to: <Text>+
given?: <Target>+
declaring?: <Target>+
using?: <Target>+
where?: <Spec>+
suchThat?: <Clause>+
if?: <Clause>+
iff?: <Clause>+
then: <Clause>+
Proof?: <ProofItemKind>+
Documented?: <DocumentedKind>+
References?: <Text>+
Aliases?: <Alias>+
Writing?: <WritingTextItem>+
Id?: <IdTextItem>
Lemma:
for: <Text>+
given?: <Target>+
declaring?: <Target>+
using?: <Target>+
where?: <Spec>+
suchThat?: <Clause>+
if?: <Clause>+
iff?: <Clause>+
then: <Clause>+
Proof?: <ProofItemKind>+
Documented?: <DocumentedKind>+
References?: <Text>+
Aliases?: <Alias>+
Writing?: <WritingTextItem>+
Id?: <IdTextItem>
Theorem:
given?: <Target>+
declaring?: <Target>+
using?: <Target>+
where?: <Spec>+
suchThat?: <Clause>+
if?: <Clause>+
iff?: <Clause>+
then: <Clause>+
Proof?: <ProofItemKind>+
Documented?: <DocumentedKind>+
References?: <Text>+
Aliases?: <Alias>+
Writing?: <WritingTextItem>+
Id?: <IdTextItem>

Resources

Resource: <ResourceKind>+
Id?: <IdTextItem>
ResourceKind ::= description:
               | title:
               | type:
               | url:
               | volume:
               | month:
               | offset:
               | publisher:
               | author:
               | edition:
               | editor:
               | homepage:
               | institution:
               | journal:
               | year:
description: <Text>
title: <Text>
type: <Text>
url: <Text>
volume: <Text>
month: <Text>
offset: <Text>
publisher: <Text>
author: <Text>
edition: <Text>
editor: <Text>
homepage: <Text>
institution: <Text>
journal: <Text>
year: <Text>

Configuration

Specify: <SpecifyKind>+
Id?: <IdTextItem>
SpecifyKind ::= positiveFloat:
              | positiveInt:
              | negativeFloat:
              | negativeInt:
              | zero:
positiveFloat:
means: <Spec>
positiveInt:
means: <Spec>
negativeFloat:
means: <Spec>
negativeInt:
means: <Spec>
zero:
means: <Spec>

People

Person: <PersonKind>+
Id?: <IdTextItem>
PersonKind ::= name:
             | biography:
name: <Text>+
biography: <Text>

Documented

DocumentedKind ::= overview:
                 | related:
                 | written:
                 | called:
                 | writing:
overview: <Text>+
related: <Text>+
written: <Text>+
called: <Text>+

TODO: specify that writing: excepts a text of the form “… :~> …”

writing: <Text>+

Provides

TODO: UPDATE THIS SO TRACKS USES *? for example for the operator TODO: UPDATE THE NAME OF THIS AND SUPPORT THINGS OF THE FORM * R(x) * X.f(x) * X.f{x} * X.f[x]{y} * X.f[x]{y : z} * X.f[x]{y | z} * X.f[x]{y : z | w}

symbol: <Alias>
tracks?: <Formulation>
replaces?: <Formulation>
written?: <Text>+
view:
as: <Target>
using?: <Target>+
where?: <Spec>+
through?: <Formulation>
signifies?: <Formulation>
encoding:
as: <Target>
using?: <Target>+
where?: <Spec>+
through?: <Formulation>

Justified

JustifiedKind ::= by:
                | label:
by: <ProofItem>+
label: <Text>
by: <ProofItem>+

Proofs

Structuring Constructs

ProofItemKind ::= block:
                | remark:
                | partwise:
                | casewise:
                | stepwise:
                | withoutLossOfGenerality:
                | forContradiction:
                | forInduction:
                | forContrapositive:
                | claim:
                | suppose:
                | sufficesToShow:
                | toShow:
                | exists:
                | exists:
                | existsUnique:
                | forAll:
                | declare:
                | because:then:
                | by:then:
                | hence:
                | next:
                | notice:
                | then:
                | therefore:
                | thus:
                | oneOf:
                | allOf:
                | anyOf:
                | equivalently:
                | if:
                | iff:
                | not:
                | absurd:
                | contradiction:
                | done:
                | qed:
                | matching:
block: <ProofItemKind>+
remark: <text>
partwise:
part+: <ProofItemKind>+
casewise:
case+: <ProofItemKind>+
else?: <ProofItemKind>+
stepwise: <ProofItemKind>+
withoutLossOfGenerality: <ProofItemKind>+
forContradiction: <ProofItemKind>+
forInduction: <ProofItemKind>+
forContrapositive: <ProofItemKind>+

Inductive

Matching

TODO: add support for this

matching: <Target>
as?: <Type>
against: <ProofMatchingCase>+

ProofMatchingCase:

case: <... := ...>
using?: <Target>+
then: <ProofItemKind>

Introductory Constructs

claim:
given?: <Target>+
using?: <Target>+
where?: <Spec>+
suchThat: <Clause>+
iff?: <Clause>+
then: <Clause>+
Proof?: <ProofItemKind>+
suppose: <ProofItemKind>+
then: <ProofItemKind>+
sufficesToShow: <ProofItemKind>+
toShow: <ProofItemKind>+
observe: <ProofItemKind>+

Symbol Introduction Constructs

exists: <Target>+
using?: <Target>+
where?: <Spec>+
suchThat: <ProofItemKind>+
existsUnique: <Target>+
using?: <Target>+
where?: <Spec>+
suchThat: <ProofItemKind>+
forAll: <Target>+
using?: <Target>+
where?: <Spec>+
suchThat?: <Clause>+
then: <ProofItemKind>+
declare: <Target>
using?: <Target>+
where?: <Spec>+
suchThat?: <Clause>+
then: <ProofItemKind>+

Reasoning Constructs

because: <ProofItemKind>+
then: <ProofItemKind>+
by: <ProofItemKind>+
then: <ProofItemKind>+

Flow of Thought Constructs

hence: <ProofItemKind>+
by?/because?: <ProofItemKind>+
next: <ProofItemKind>+
by?:/because?: <ProofItemKind>+
notice: <ProofItemKind>+
by?:/because?: <ProofItemKind>+
then: <ProofItemKind>+
by?:/because?: <ProofItemKind>+
therefore: <ProofItemKind>+
by?:/because?: <ProofItemKind>+
thus: <ProofItemKind>+
by?:/because: <ProofItemKind>+

Logical Constructs

oneOf: <ProofItemKind>+
allOf: <ProofItemKind>+
anyOf: <ProofItemKind>+
equivalently: <ProofItemKind>+
if: <ProofItemKind>+
then: <ProofItemKind>+
iff: <ProofItemKind>+
then: <ProofItemKind>+
not: <ProofItemKind>

Terminating Constructs

absurd:
contradiction:
done:
qed:

Labels

Declaring

TODO: update this to use {..}

'{.{.x + 1.}(1) + y.}(some.label)'
'{.x+1.}(1)'

can be written as

'x + 1'  (1)
[some.label]
exists: x
where: '...'
suchThat: '...'

Referencing

TODO: Update this

In addition to the following, the \\definition:of:satisfies builtin can be used as a reference:

\:a.b.c:d:e::(some.label)
\:a.b.c{x}:d{y}:e::(some.label)
\(some.label)
\some.theorem::(some.label)
\some.theorem:given{x, y}::(some.label)

Writing

Overview

TODO: update this to use :~> and to support symbols

"target :~> latex"
"epsilon :~> \varepsilon"
"a(i) :~> a?_{i?}"
"Delta$x :~> \Delta_{$x}"

writing: uses the same replacement rules as written:

Written

Overview

x?
x+?
x-?
x=?
x?{... suffix}
x?{prefix ...}
x?{... infix ...}
x? is the same as x-?

Sigils

Order of operations

Type checking

Symbol Resolution

Encoded As

Viewed As

f(x, y, z) interpretation

TODO: update this to describe :=:

TODO: update this to properly describe varargs. ie f(x…) in a definition means the definition auto interprets multiple args as a tuple while f(x) expects one arg (that could be a tuple) and f((x…)) expects a tuple of potentially multiple items, f(x, y) expects two items and f((x, y)) expects one tuple with two items

f(…(x, y)) f(…x)

The following all mean the same:

X := (x, y)
f(X)
f((x, y))
f(x, y)

that is the tuple is automatically collapsed. This aligns with common math usage. Note: this only works for function calls. That is \foo{(x, y)} and \foo{x, y} are not the same.

Functions and Operators

The forms x * y and "*"(x, y) are treated as the same. The same is true for -x and "-"(x) as well as x! and "!"(x).

This means if -x and x- are both operators in scope then the form "-"(x) cannot be used since it is ambiguous. In this case , one of -x and x- should be changed, or an alias made to distinguish one form to another if "-"(x) needs to be used.

Symbol Resolution

TODO

The next section is out of date TODO update it to describe the use of the tracks: section.

Update * to use *? which means the x *? y is dynamic. That is, if G := (Y, +, 0) is \group' then x * y is not available but x + y is.

[\group]
Describes: G := (X, *, e)
Provides:
. 'x [.in.]: G :-> x is \element.of:set{G}'


[\element.of:{G}]
Describes: x
when: 'G is \group'
Provides:
. 'x *? y :=> x [.G.*?.] y'

Add support for #some.theorem, #!some.axiom and #?some.conjecture.

TODO: add support for \?command and \?operator?/

TODO: add the Legend: or Write: group and finalize its name

Variadic Arguments and Automatic Tuple Creation

TODO: Update logic for varargs and auto-tuple creation

The ...x syntax is used to specify that the tuple described by x should be flattened out. So if z := (x, y) then f(...z) means f(x, y).

In a function definition the prefix ... is used to specify that a tuple is automatically un-flattened. That is f(x, y) is interpreted as f((x,y)). Specifically:

TODO: update this to describe :=: instead of …x which is not used anymore

f(x) means f takes one argument x
f((x...)) means f takes one argument that is a tuple with any number of args
f(...(x...)) means f takes one tuple argument with any number of args
             but f(x,y,z) is interpreted as f((x,y,z))
             Note: the ...x syntax can only be used for tuples
                   so f(...x) or f(...g(x)) are not valid.
f(x, y) means f takes exactly two arguments x and y
f((x, y)) means f takes one argument which is a tuple with two arguments
f(...(x, y)) means f takes one argument which is a tuple with two arguments
             but f(x, y) is interpreted as f((x, y))
f(x...) means f takes any number of arguments
        (they are not interpreted as a tuple)
        Instead, f(...(x...)) specifies x takes any number of arguments
        that should be interpreted as a tuple
f(g(x)...) means f takes any number of arguments that are all of the
           shape g(x)
           g(x)[i] references the ith one
f((x,y)...) means f takes any number of arguments that are all tuples
            of the form (x, y) where (x, y)[i] references the ith one
etc.

If a definition or describes states the shape of the thing being defined is of the form f(...(x...)) then f(x) is interpreted in a couple ways. If x is a tuple then it is then input to f otherwise if it is not, then it is interpreted as a tuple with one element.


 =
!=
:=
:=>
:=:
:-
:->
:~>
==

TODO

Provides:
. comparison: "\function:on{A}:to{B} is \function:on{X}:to{Y}"
  provided:
  . "X is A"
  . "B is Y"

that allows one to specify if a type is covariant, contravariant, or requires strict equality of types. The provided can be of the form X is A or X = A where X = A means X is A and A is X.

Also, one can have tuples on the right hand side of the is. For example, in a definition of \R2 one could have:

[\R2]
Describes: (x, y)
...
Provides:
. comparison: "(x, y) is \R2"
  provided:
  . "x, y is \real"

This allows one to use f((x,y)) where x,y is \real instead of f(x, y) if the function is defined to support f(x...) :=: f((x...)).




\matrix{1, 2, 3}
       {4, 5, 6}

\R{3}

x [.in.]: \R{n}

\matrix{x{(i,j)...(m,n)}}
\vector{x{i...n}}

\real.vector{1, 2, 3}

\integral[x]{f[x]}:d{$x}
\integral[x,y]{f[x,y]}:d{$x, $y}
\integral[x,y]{f[x,y]}:d{$y, $x}
\integral[x,y]{f[x,y]}:d{$x}
\integral[x,y]{f[x,y]}:d{$x}


\integral[u,v]{u^2 + v^2}:d{$u}

\definite.riemann.integral[x]{\sin(x) + \sin2(x)}:d{$x}:from{0}:to{1}

\int[x]{f[x]}:on{a, b} :=>
  \definite.riemann.integral[x]{f[x]}:d{$x}:from{a}:to{b}

\int[u]{\sin(u)}:on{0, \pi}