Open gallais opened 1 year ago
Very nice.
A lot of proofs in agda-categories could be made more digestible for humans with such machinery, as quite a lot of work is spent on dealing with cong and re-associating to put a part "in focus". For efficiency, I'd probably want proof-emitting macros rather than using them directly in library code. But that seems most doable. At the level of, say, monoidal categories, such proof-emitting macros might even be a papers' worth of work.
Hello there.
I just opened #2310 without realizing that #2033 existed, which looks more elegant than my hack on top of cong!
.
What's the plan going forward with this? Happy to withdraw my proposal, if this is still being worked on.
I have written a little bit of declarative congruence magic:
https://github.com/gallais/potpourri/blob/b0b734fb8e768f280bc36519048b977b994d1a5e/agda/cong/Syntax/Focus.agda
Unlike the content of
Tactic.Cong
, it is not trying to guess what the context should be but instead reads it off the goal type where users can mark the focus of their action by using the⟪_⟫
focus.