summaryrefslogtreecommitdiff
path: root/Nominal/Instances
AgeCommit message (Collapse)Author
2026-04-15fs constructionsHannes Schulze
2026-04-15update leanHannes Schulze
2025-12-05define algebrasHannes Schulze
2025-12-04implement derivable equalityHannes Schulze
2025-12-03refactor equivariant props to use type classesHannes Schulze
2025-12-02minor cleanupHannes Schulze
2025-11-20wip termsHannes Schulze
2025-10-30prove supp of 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-23refactor: move instancesHannes Schulze
generated by cgit v1.3.1 (git 2.54.0) at 2026-11-10 10:51:37 +0000