diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2022-07-07 17:53:24 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2022-07-07 17:53:24 +0100 |
| commit | 2147acd780ca4586a4fd7b045eb92611cdbb13a0 (patch) | |
| tree | 7a07f466a44b028fc506a636e134f60e420b65e6 /src/Data/Util.agda | |
| parent | 07c4a784b46f6cfe47d1c37329051b4b5d459755 (diff) | |
Prove alpha equivalence preserves free variables.
Diffstat (limited to 'src/Data/Util.agda')
| -rw-r--r-- | src/Data/Util.agda | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/Data/Util.agda b/src/Data/Util.agda new file mode 100644 index 0000000..4d9ec33 --- /dev/null +++ b/src/Data/Util.agda @@ -0,0 +1,13 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Util where + +open import Data.List using (List) +open import Data.List.Membership.Propositional using (_∉_) +open import Data.Nat using (ℕ) + +record IsFresh (mkFresh : List ℕ → ℕ) : Set where + field + distinct : ∀ αs → mkFresh αs ∉ αs + +open IsFresh public |