haschu/nominal-lean.git/Nominal/Equivariance.lean, branch name-restriction-model Formalization of nominal sets in Lean 4. https://git.haschu.me/haschu/nominal-lean.git/atom/Nominal/Equivariance.lean?h=name-restriction-model 2025-12-03T19:34:41Z 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 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 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 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 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