summaryrefslogtreecommitdiff
path: root/Nominal
AgeCommit message (Expand)Author
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-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-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-23add category definitionHannes Schulze
2025-10-23refactor: move instancesHannes Schulze
2025-10-23add equivariant instancesHannes Schulze
2025-10-23define equivarianceHannes Schulze
2025-10-23add freshnessHannes Schulze
2025-10-22always require infinite, countable, equality-decidable atomsHannes Schulze
2025-10-22update importsHannes Schulze
2025-10-22add product and coproduct instancesHannes Schulze
2025-10-22some helper lemmas for fixHannes Schulze
2025-10-22further simplificationsHannes Schulze
2025-10-21Restructure support_inter proofHannes Schulze
2025-10-21restructureHannes Schulze
2025-10-21very rough draft for support_interHannes Schulze
2025-10-21simplify some moreHannes Schulze
2025-10-21add some proofs about specific least supportsHannes Schulze
2025-10-20some simplificationsHannes Schulze
2025-10-20prove things about intersections and supportsHannes Schulze
2025-10-20Prove nonempty induction on finsetsHannes Schulze
2025-10-20further workHannes Schulze
2025-10-20further work on nominal set definitionHannes Schulze
generated by cgit v1.3.1 (git 2.54.0) at 2026-11-10 14:40:44 +0000