implement lambda preterms

1 files changed, 12 insertions, 0 deletions

diff --git a/Nominal/Helpers/CountableString.lean b/Nominal/Helpers/CountableString.lean
new file mode 100644
index 0000000..7d2fcb7
--- /dev/null
+++ b/Nominal/Helpers/CountableString.lean
@@ -0,0 +1,12 @@
+import Mathlib
+
+instance : Countable Char where
+  exists_injective_nat' := by
+    exists Char.toNat
+    intro c₁ c₂ hc
+    rw [Char.toNat, Char.toNat, UInt32.toNat_inj] at hc
+    exact Char.eq_of_val_eq hc
+
+instance : Countable String := Countable.of_equiv (List Char)
+  { toFun := String.mk
+    invFun := String.data }