| Age | Commit message (Collapse) | Author |
|---|
|
Parameters must follow the relation symbol and be surrounded by braces, like so: `\rel{x}{y}{z}`.
This attempt is still brittle/broken in a few ways:
- It makes using braces in creative ways in mixfix notation ambiguous.
- It does not verify that the parameters are used in a consistent manner for each symbol. It essentially allows users to define `a\MyRel b` and `a\MyRel{x} b` (and ones with even more parameters).
- It allows parameters for all relation symbols, even for those where it makes no sense in ordinary TeX markup, e.g. `a <{x} b`.
|
|
Use an `\iff`-calc to speed up `union_as_unions`. Also remove `in_implies_neq` which seems to interact badly with the choice axiom used by superposition-based proofs like Vampire in cut-down problems.
|
|
|
|
Since Latex has a really specify syntax for
\begin{cases} ... \end{cases}
The math mode in tokenizing had to be setup correctly.
|
|
since now some could define a function with overlapping
and worng subdomains
|
|
But the Proof that the domain of the local function
is not right. Also if in the definition of our local
function we just use f(x) = x then we get a technical
ambigus parse
|
|
|
|
for local functions and a abstract type in abstract.hs
for the proof data structure.
|
|
|
|
|
|
|
|
|
