summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2026-01-23name restrictionsname-restriction-modelHannes Schulze
2026-01-16add fmap for M_0 algebra morphismsHannes Schulze
2026-01-13add M_1 model structureHannes Schulze
2026-01-12prove well-definedness of absHannes Schulze
2026-01-12cleanupHannes Schulze
2026-01-12prove depth-0 axiomsHannes Schulze
2026-01-11prove some more axiomsHannes Schulze
2026-01-11prove well-definedness of restrict operationHannes Schulze
2026-01-10well-definedness of unionHannes Schulze
2026-01-10add model at depth 0Hannes Schulze
2025-12-05Alg categoryHannes Schulze
2025-12-05revise OrbitFinite restriction for equationsHannes Schulze
2025-12-05define algebrasHannes Schulze
2025-12-04fix depthHannes Schulze
2025-12-04prove that derivable equality is an equivariant equivalenceHannes Schulze
2025-12-04implement derivable equalityHannes Schulze
2025-12-03more cleanupHannes Schulze
2025-12-03differentiate bw substitution and uniform substitutionHannes Schulze
2025-12-03clean up nominal algebra termsHannes Schulze
2025-12-03refactor equivariant props to use type classesHannes Schulze
2025-12-02start defining nominal algebra termsHannes Schulze
2025-12-02formalize graded monadsHannes Schulze
2025-12-02minor cleanupHannes Schulze
2025-12-01finish initial lambda terms modulo alpha-equivalenceHannes Schulze
2025-12-01prove pick_freshHannes Schulze
2025-11-30update leanHannes Schulze
2025-11-20wip termsHannes Schulze
2025-10-30prove supp of pretermsHannes Schulze
2025-10-30implement lambda pretermsHannes Schulze
2025-10-29refactor equivariance namespacesHannes Schulze
2025-10-28name abstraction functorHannes Schulze
2025-10-28restructure alpha equivalenceHannes Schulze
2025-10-28finish name abstraction supp proofHannes Schulze
2025-10-28more wipHannes Schulze
2025-10-27wip: name abstractions form a nominal setHannes Schulze
2025-10-27quotient types as nominal setsHannes Schulze
2025-10-26finish name abstraction proofsHannes Schulze
2025-10-26simplify FPerm computationsHannes Schulze
2025-10-25start working on alpha equivalence proofsHannes Schulze
2025-10-24use simp only everywhere except for last goalHannes Schulze
2025-10-24show properties for freshness quantifier based on equivariant relationsHannes Schulze
2025-10-24fill in some proofsHannes Schulze
2025-10-24proof sketch for proving different AlphaEq characterizationsHannes Schulze
2025-10-24refactor namespacesHannes Schulze
2025-10-23basic structure for name abstractionHannes Schulze
2025-10-23add forgetful functorsHannes Schulze
2025-10-23update root moduleHannes Schulze
2025-10-23add category definitionHannes Schulze
2025-10-23refactor: move instancesHannes Schulze
2025-10-23add equivariant instancesHannes Schulze
generated by cgit v1.3.1 (git 2.54.0) at 2026-11-10 10:20:00 +0000