Mike Gerwitz
e70933eef8
design/tpl (Vectors and Index Sets): Refinement and rectangular matrix intro
...
This refines the section a bit and introduces the familiar notation for
rectangular matrices (which normal people just call "matrices").
2021-05-21 16:10:44 -04:00
Mike Gerwitz
8edef8a8c8
design/tpl (\rank): Add macro
2021-05-20 15:28:10 -04:00
Mike Gerwitz
50a6ccf4ec
design/tpl (Classification System): Equation number refinement
...
Just clean up a little bit using more proper AMS environments.
2021-05-20 15:22:06 -04:00
Mike Gerwitz
98d724a7d7
design/tpl (Vectors and Index Sets): Remove unique value set example
...
This ended up not being needed for the definition of the classification
system and just adds noise.
2021-05-20 12:42:51 -04:00
Mike Gerwitz
7d0402d350
src/current/doc: Remove
...
This represents the old cmatch system (which is in use today, but the
classification system has since been rewritten, though it has not yet been
merged). It was my attempt over a decade ago to reason about how this
system ought to work.
I think it's fair to say that this is absolute insanity and that the new
formulation is significantly better.
2021-05-20 11:25:32 -04:00
Mike Gerwitz
9ad144d3d4
design/tpl (Classification System): Initial match definition
...
This is a bit raw; it needs some explanation and examples.
2021-05-20 10:45:44 -04:00
Mike Gerwitz
0d59ff607e
design/tpl (XML Notation): Add additional example for literal binding
2021-05-19 13:06:40 -04:00
Mike Gerwitz
f71c58b1da
design/tpl (Vectors and Index Sets) [Rank]: New definition
2021-05-19 12:58:20 -04:00
Mike Gerwitz
aafebbc716
design/tpl: Classification index entries
2021-05-19 10:48:35 -04:00
Mike Gerwitz
5fdaecf765
design/tpl: Adjust \footheight
...
KOMA-Script is complaining, because of the multi-line Copyright notice on
the first page. This resolves that warning.
2021-05-19 10:05:36 -04:00
Mike Gerwitz
4a6f44ff90
design/tpl: Formatting of source files
...
This introduces missing license headers in files and better organizes
tpl.sty into sections.
2021-05-19 10:05:29 -04:00
Mike Gerwitz
dfdf92848a
design/tpl (Classification Introduction): Codomain {Real=>Bool}
...
Whoops. The values of the params are reals, but predicates are all
booleans, having been first transformed by the yet-to-be-formally-defined
matches.
2021-05-19 09:02:48 -04:00
Mike Gerwitz
f5b2261f0d
design/tpl: Euler font
...
I removed this when I added concmath, thinking that it would include it for
me, and apparently I never re-added it after realizing that it didn't.
I'm a big fan of the typography of Concrete Mathematics.
2021-05-18 16:28:43 -04:00
Mike Gerwitz
a488e3549d
design/tpl (Classification System): Intro src formatting
...
Just aligning. Meant to do this in the previous commit.
2021-05-18 16:15:05 -04:00
Mike Gerwitz
bf6cf96169
design/tpl (Classification System): Reduce height for intro vdots
...
The subscript of the matrix family adds too much vertical space. This
offsets that to restore it to about what it otherwise would be, since the
second subscript does not get in the way.
2021-05-18 16:14:10 -04:00
Mike Gerwitz
158e045762
design/tpl: geometry package for letterpaper
...
Was not working properly in vanilla TeX Live image.
2021-05-18 16:03:06 -04:00
Mike Gerwitz
d65c061b29
design/tpl: configure script (for appendix)
...
It's not required; TPL will fall back when missing conf.tex.
2021-05-18 15:56:25 -04:00
Mike Gerwitz
80fd239d95
design/tpl: Letter paper
...
This is what we'll usually be printing on, after all.
2021-05-18 15:06:35 -04:00
Mike Gerwitz
83e3ade149
design/tpl (Classification System)[Classification Yield]: Allow break after "then"
...
This was rendering poorly, breaking instead in the middle of "Axiom".
2021-05-18 14:15:52 -04:00
Mike Gerwitz
ef231f89fa
design/tpl (Classification System): Remove TODO for always/never
...
This was done in the previous commit.
2021-05-18 14:11:40 -04:00
Mike Gerwitz
8957e6caf0
design/tpl (Classification System): Add always and never figure
...
This demonstrates the vacuity lemma.
2021-05-18 14:09:27 -04:00
Mike Gerwitz
dfa37f5b77
design/tpl: Use \{emph=>dfn} for term introductions
...
This uses \textsl rather than \emph.
2021-05-18 12:16:11 -04:00
Mike Gerwitz
8a2407d66f
design/tpl: Emphasize commutativity of monoids in classification system
2021-05-18 12:13:58 -04:00
Mike Gerwitz
1ec0fc0c7b
design/tpl (Notational Convetions): Clean up unneeded bicompi
...
This was originally going to be used to define @yields for the classifier,
but I took a very different approach which doesn't require reasoning about
the system in terms of recursion.
2021-05-18 10:16:06 -04:00
Mike Gerwitz
2d268f2a55
design/tpl: Initial definition of classifications
...
This defines @as and @yields, but does not yet define matches formally.
It's also missing index entries, which I'll take the time to add after I'm
sure things are staying as they are.
This was quite a bit of work, and the approach I took is different than I
originally expected, so Section 0 can use some cleanup.
There is more to come from here.
2021-05-18 10:09:29 -04:00
Mike Gerwitz
4ea2574a8c
design/tpl/tpl.sty: Use autoref for theorem macros
2021-05-17 13:21:56 -04:00
Mike Gerwitz
fbe76a5616
design/tpl: Beginnings of classifications in terms of first-order logic
...
This is going to evolve a great deal, and note that the yield definition is
completely absent.
It may be time to switch to natural deduction (Gentzen-style).
2021-05-14 12:14:11 -04:00
Mike Gerwitz
9bcd7e1d7e
design/tpl: Abstract theorem env + label creation
2021-05-14 10:50:49 -04:00
Mike Gerwitz
9fd57872ed
design/tpl (Monoids and Sequences): Add missing index entries
...
Forgot in previous commit.
2021-05-14 10:38:17 -04:00
Mike Gerwitz
8d54420656
design/tpl (Monoids and Sequences): New section
2021-05-14 10:34:13 -04:00
Mike Gerwitz
060a7d0e6c
design/tpl: \{log=>l}{and,or}
...
Don't I feel silly.
2021-05-14 10:34:09 -04:00
Mike Gerwitz
63b502b7df
design/tpl: Add ccicons for Copyright line
2021-05-12 10:37:20 -04:00
Mike Gerwitz
1ad6bc93d7
design/tpl (Meta: Typesetting): Correct use of \tameclass
...
That macro previously expanded into \Classify, but that was undone before
committing to make it clear when one is referring to a variable vs. a
classification as a definition.
2021-05-11 16:52:03 -04:00
Mike Gerwitz
3cb2726737
desgin/tpl: Appendices begin on a new page
2021-05-11 16:50:23 -04:00
Mike Gerwitz
bff2b32a52
design/tpl: More TODOs and margin remarks
2021-05-11 16:50:11 -04:00
Mike Gerwitz
9d9535a1b8
design/tpl: Introduce \Classify mathop
...
This will be used as an IR of sorts to eliminate the XML, which will be far
too verbose to use in proofs. It also allows us to attach behavior to the
operator, which will end up defining two values for @as and @yields.
2021-05-11 16:37:08 -04:00
Mike Gerwitz
d78186461f
desgin/tpl: Add \todo margin notes
2021-05-11 16:36:43 -04:00
Mike Gerwitz
08109bc35d
design/tpl: Vector addition example: \bicomp{=>i}
...
The example as presented was incorrect, since \bicomp is undefined for
scalar values.
2021-05-11 13:49:18 -04:00
Mike Gerwitz
7735ba1f29
design/tpl: Remove \exists from classification definitions
...
The previously-existing notation for this has been removed. These will be
updated soon to account for vectors and matrices, but until then, this is
simply nonsense.
2021-05-11 13:28:02 -04:00
Mike Gerwitz
d49133e8e9
design/tpl: (Disjunctive Classification): Footnote formatting correction
...
Missing `,' in the \forall set.
2021-05-11 13:24:20 -04:00
Mike Gerwitz
51c87f9938
design/tpl: Reposition disjunctive classification footnote
...
The original position made it look to much like d^2.
2021-05-11 13:21:05 -04:00
Mike Gerwitz
6dc0ca2454
design/tpl: Show listings in draft mode
...
What an odd default.
2021-05-11 13:08:25 -04:00
Mike Gerwitz
5808afc8a2
design/tpl: Universal=>conjunctive, existential=>disjunctive classification
2021-05-11 13:06:06 -04:00
Mike Gerwitz
2407af56e4
design/tpl: _-notation clarification (wildcard/hole)
2021-05-11 12:47:28 -04:00
Mike Gerwitz
13317aac6c
design/tpl: Vectors and Index Sets \goodbreak
...
This fits nicely on a single page. At the time of writing, the previous
section is near the end of the page, so this works reasonably well.
2021-05-11 11:39:23 -04:00
Mike Gerwitz
7f4fc8e3b7
design/tpl: Mostly-complex symbol index entries for Chapter 0
2021-05-11 11:33:12 -04:00
Mike Gerwitz
7624bd2958
design/tpl: TAMER case fix
...
'T' was lowercased.
2021-05-11 11:32:19 -04:00
Mike Gerwitz
02335f9a4a
design/tpl: Clear copyright on Index pages
...
Apparently index page output uses a different even/odd determination than
the normal article page output.
2021-05-11 11:31:27 -04:00
Mike Gerwitz
dfb013ca74
design/tpl: Corrected conjunction/disjunction index placement
...
They were incorrectly placed at the quantifiers.
2021-05-11 09:59:03 -04:00
Mike Gerwitz
cb9ccfe5f3
design/tpl: \vdash=>\infer and index entry
2021-05-10 16:54:19 -04:00
Mike Gerwitz