summaryrefslogtreecommitdiff
path: root/Nominal/Equivariance.lean
AgeCommit message (Expand)Author
2026-04-15update leanHannes Schulze
2025-12-03refactor equivariant props to use type classesHannes Schulze
2025-10-30prove supp of pretermsHannes Schulze
2025-10-29refactor equivariance namespacesHannes Schulze
2025-10-28name abstraction functorHannes Schulze
2025-10-27quotient types as nominal setsHannes Schulze
2025-10-26finish name abstraction proofsHannes 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-24proof sketch for proving different AlphaEq characterizationsHannes Schulze
2025-10-23add forgetful functorsHannes Schulze
2025-10-23add equivariant instancesHannes Schulze
2025-10-23define equivarianceHannes Schulze