haschu/nominal-lean.git/Nominal/Permutations.lean, branch graded-algebra Formalization of nominal sets in Lean 4. https://git.haschu.me/haschu/nominal-lean.git/atom/Nominal/Permutations.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 implement derivable equality 2025-12-04T16:14:46Z Hannes Schulze haschu0103@outlook.de 2025-12-04T16:14:46Z urn:sha1:8fdf459876b999dbe184196f9abd330a3c24d560 wip terms 2025-11-20T10:56:18Z Hannes Schulze haschu0103@outlook.de 2025-11-20T10:56:18Z urn:sha1:ea38ef0cb2c57e10696c7fb6108732a6f454818c more wip 2025-10-28T13:56:12Z Hannes Schulze haschu0103@outlook.de 2025-10-28T13:56:12Z urn:sha1:6b8b43eedf972cbfff8c97657a0a6a1300dcb140 quotient types as nominal sets 2025-10-27T20:58:56Z Hannes Schulze haschu0103@outlook.de 2025-10-27T20:58:56Z urn:sha1:b3f26f306945ec9e391140f1645012ba11decb40 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 start working on alpha equivalence proofs 2025-10-24T23:07:56Z Hannes Schulze haschu0103@outlook.de 2025-10-24T23:07:56Z urn:sha1:c3700706466cb8fb9ed287ea066b656caacdc9c7 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