summaryrefslogtreecommitdiff
path: root/Common/Helpers.lean
diff options
context:
space:
mode:
authorAndreas Grois <andi@grois.info>2023-12-01 23:21:14 +0100
committerAndreas Grois <andi@grois.info>2023-12-01 23:30:43 +0100
commit24d7fab85b2eb1b7996fd0ceccdd0377f1ce087b (patch)
tree2295b86307d2e5e6fbb59f009d84a635d74ef096 /Common/Helpers.lean
Day 1
Diffstat (limited to 'Common/Helpers.lean')
-rw-r--r--Common/Helpers.lean2
1 files changed, 2 insertions, 0 deletions
diff --git a/Common/Helpers.lean b/Common/Helpers.lean
new file mode 100644
index 0000000..f57f826
--- /dev/null
+++ b/Common/Helpers.lean
@@ -0,0 +1,2 @@
+def curry (g : (α × β) → γ) : α → β → γ := λ a b ↦ g (a,b)
+def uncurry (f : α → β → γ) : (α × β) → γ := λ (a,b) ↦ f a b