Skip to content

Improve string elim - #17

Merged
jacobneu merged 53 commits into
mainfrom
improveStringElim
May 7, 2026
Merged

Improve string elim#17
jacobneu merged 53 commits into
mainfrom
improveStringElim

Conversation

@jacobneu

@jacobneu jacobneu commented May 7, 2026 •
edited
Loading

Copy link
Copy Markdown
Owner
  • Split different string output formats (pseudoAgda, Forester)
  • Implemented SectStr

jacobneu added 30 commits March 16, 2026 18:56
@jacobneu
Init Forester printing; got algebras and context working
b5a3a74
@jacobneu
Got DAlg basically working; some minor issues to fix
068c2d4
@jacobneu
Made more principled tex data type
2fe13a1
@jacobneu
Experiments with implementing Alg in the elaborator
e66b61f
@jacobneu
Cleaned up nouGAT elaborator somewhat
22bc118
@jacobneu
Commented out wellCon proofs which broke for some reason
d0a9fe1
@jacobneu
Re-added argument counting
4ea9fd7
@jacobneu
Got application typechecking working (essentially)
509c442
@jacobneu
Got elaborator typechecking working, except for transport
266d1ad
@jacobneu
Got typechecking (apparently) fully working, including CwF and PCwF (…
a4fc6e7 
…fixed some existing errors there and in Cat)
@jacobneu
Restored [GATdata| ] to producing GATdata, fixed groupoid, modified A…
5ac74c8 
…lgString and DAlgString to accept new GATdata defn
@jacobneu
Started using State monad
5a908b9
@jacobneu
Cleaned up nouGAT code
d47fdff
@jacobneu
Reimplemented nouGAT elaborator with StateT for better error messages
b57f4bd
@jacobneu
Cleaned up some comments, implemented rawMode boolean to clean up output
b2ea1e7
@jacobneu
Started implementing holes
e911b40
@jacobneu
Revert "Started implementing holes"
cd390b3 
This reverts commit 8e5a455.
@jacobneu
Split metaTy into marker & telescope
8d745e6
@jacobneu
Abstracted preCon eliminator
77700b5
@jacobneu
Moved elimination elabs into their own file
492554a
@jacobneu
Reintroduced {{ }} for GATs, elaborated as product of all eliminators
5ae78ef
@jacobneu
Added syntax for bunching arguments
a4a53f3
@jacobneu
Allowed for multi-declarations at top level, simplified con_inner
765ea70
@jacobneu
Made it possible to mark arguments as implicit (though they still hav…
b96078c 
…e to be supplied)
@jacobneu
Fixed bug with operator precedences
1735288
@jacobneu
Created rawGAT mode
0d5fc15
@jacobneu
Started principled string representation for Alg
565162e
@jacobneu
Changed signatures to {{ }}, fixed reversal bugs in Alg and Con printing
c8b32fd
@jacobneu
Created augElim to better print implicit arguments in algebra
eab9313
@jacobneu
Got DAlgString working nicely
17e457b
jacobneu added 23 commits April 8, 2026 15:35
@jacobneu
Got HomStrElim working
9581cca
@jacobneu
Added ability to supply variable names in command line
dfa1473
@jacobneu
Improved augTy to store variable name data, cleaned up String elimina…
bdd435f 
…tors
@jacobneu
Improved string handling of arguments & telescopes
ac99350
@jacobneu
Reimplemented metaArg using ArgMarker
7e4f02a
@jacobneu
Got SectStr working
b653efe
@jacobneu
Started abstracting StringFormat
6c69693
@jacobneu
String representation now basically fully abstracted
3bf4d59
@jacobneu
Utilities for presentation 2026-04-17
84e7a3b
@jacobneu
Added alternate alg names argument to XXXStr_Con functions
d07316a
@jacobneu
Fully customized the name of the algebra in DAlg, the algebra and dis…
84dab2f 
…p. alg in Sect, zero and one in Hom, etc.
@jacobneu
Incorporated StringFormat into ConString
0b80575
@jacobneu
Renamed generalizedalgebra to pseudoAgda, incorporated headings into …
9b8b2d1 
…StringFormat
@jacobneu
Made format headings (possibly) multi-line
04f24fd
@jacobneu
Fixed bug in paren'; use SF.paren in ConString
8a5a301
@jacobneu
Added plain-string GAT name as argument to formatWrapping
907dc5d
@jacobneu
Added parens around El argument in ConString
2559e17
@jacobneu
Added StringFormat field for modifying identifiers
24ddd75
@jacobneu
Got forester working; used in 2026-04-27 version of genalg forester b…
6f7208e 
…uilds
@jacobneu
Added SF.breakOpportunity to insert breaks; renamed some components i…
3e360d1 
…n CwF
@jacobneu
Merge branch 'improveStringElim' into forester
999f0c2
@jacobneu
Cleaned up Forester presentation, particularly with line breaks
c6ad3f4
@jacobneu
Merge branch 'main' of https://github.com/jacobneu/GeneralizedAlgebra …
493383d 
…into improveStringElim
@jacobneu
jacobneu merged commit d2f4029 into main May 7, 2026
0 of 2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@jacobneu