haschu/nominal-lean.git/Nominal/Instances/Abstraction.lean, branch graded-algebra Formalization of nominal sets in Lean 4. https://git.haschu.me/haschu/nominal-lean.git/atom/Nominal/Instances/Abstraction.lean?h=graded-algebra 2026-04-15T11:22:40Z update lean 2026-04-15T11:22:40Z Hannes Schulze contact@haschu.me 2026-04-14T14:04:44Z urn:sha1:a5ff8efe5b5e314e0aa759318e5fb194e066f612 refactor equivariant props to use type classes 2025-12-03T19:34:41Z Hannes Schulze haschu0103@outlook.de 2025-12-03T19:34:41Z urn:sha1:71a6a3d5b6f4b428b463bc4a0766c91d8c1d5768 minor cleanup 2025-12-02T10:52:55Z Hannes Schulze haschu0103@outlook.de 2025-12-02T10:52:15Z urn:sha1:a8915795c109980285e11ed53d453987c0917069 prove supp of preterms 2025-10-30T12:11:43Z Hannes Schulze haschu0103@outlook.de 2025-10-30T12:11:43Z urn:sha1:80b248c5be656dd2b3ba753871aeeb7102e92ff8 refactor equivariance namespaces 2025-10-28T23:40:13Z Hannes Schulze haschu0103@outlook.de 2025-10-28T23:40:13Z urn:sha1:5dde77b6db9fc78094363f91e0c6643a84be513e name abstraction functor 2025-10-28T22:41:02Z Hannes Schulze haschu0103@outlook.de 2025-10-28T22:41:02Z urn:sha1:8f1d3f45f11aae5d611a66c424b6427f379a8251 restructure alpha equivalence 2025-10-28T20:42:07Z Hannes Schulze haschu0103@outlook.de 2025-10-28T20:42:07Z urn:sha1:1bc59fecb46835983850e2ee982073614868eaca finish name abstraction supp proof 2025-10-28T20:22:28Z Hannes Schulze haschu0103@outlook.de 2025-10-28T20:22:28Z urn:sha1:9836f94b46f21f508e9acd469197ac323b87cb0a more wip 2025-10-28T13:56:12Z Hannes Schulze haschu0103@outlook.de 2025-10-28T13:56:12Z urn:sha1:6b8b43eedf972cbfff8c97657a0a6a1300dcb140 wip: name abstractions form a nominal set 2025-10-27T21:26:48Z Hannes Schulze haschu0103@outlook.de 2025-10-27T21:26:48Z urn:sha1:4d52488841dd687bc0ffd0f468bae1ab64f495fc