haschu/nominal-lean.git/Nominal/Support.lean, branch main Formalization of nominal sets in Lean 4. https://git.haschu.me/haschu/nominal-lean.git/atom/Nominal/Support.lean?h=main 2026-04-15T14:18:47Z fs constructions 2026-04-15T14:18:47Z Hannes Schulze contact@haschu.me 2026-04-15T14:18:07Z urn:sha1:2e5f7e22761bd30857bbe067862a8b256805ecd8 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 update lean 2025-11-30T21:33:32Z Hannes Schulze haschu0103@outlook.de 2025-11-30T21:20:35Z urn:sha1:e02ad2dcc0f93107c18f8316b386b92b45548e97 finish name abstraction proofs 2025-10-26T12:31:36Z Hannes Schulze haschu0103@outlook.de 2025-10-26T12:26:57Z urn:sha1:091fd832586627fbf31375fb5487d5e6fa6f7053 simplify FPerm computations 2025-10-25T23:20:20Z Hannes Schulze haschu0103@outlook.de 2025-10-25T23:19:45Z urn:sha1:10edba2c0365a6858a74da22042c98f9d5fa1acc use simp only everywhere except for last goal 2025-10-24T16:20:43Z Hannes Schulze haschu0103@outlook.de 2025-10-24T16:20:43Z urn:sha1:6df3f662f0f23e837b70ef1f4a8b8dde4a7aa521 show properties for freshness quantifier based on equivariant relations 2025-10-24T16:05:28Z Hannes Schulze haschu0103@outlook.de 2025-10-24T16:05:28Z urn:sha1:ac2363701c3d2a03116af449ca7bc4f918fbfda7 proof sketch for proving different AlphaEq characterizations 2025-10-23T22:54:44Z Hannes Schulze haschu0103@outlook.de 2025-10-23T22:54:44Z urn:sha1:96164bc58172cbec5579e8bf38933dfb5cc51381 refactor namespaces 2025-10-23T22:15:26Z Hannes Schulze haschu0103@outlook.de 2025-10-23T22:15:26Z urn:sha1:52da7e6960ea5eedb7374be07aa065a8f34128b8