3 files changed, 94 insertions, 0 deletions
diff --git a/entries/funemy/.gitignore b/entries/funemy/.gitignore
new file mode 100644
index 0000000..acb903a
--- /dev/null
+++ b/entries/funemy/.gitignore
@@ -0,0 +1,3 @@
+.DS_Store
+*.agdai
+*.smt2
diff --git a/entries/funemy/agda/fib1.agda b/entries/funemy/agda/fib1.agda
new file mode 100644
index 0000000..d8931a0
--- /dev/null
+++ b/entries/funemy/agda/fib1.agda
@@ -0,0 +1,34 @@
+open import Agda.Builtin.Equality
+
+data Nat : Set where
+  zero : Nat
+  suc : Nat -> Nat
+
+{-# BUILTIN NATURAL Nat #-}
+
+z : Nat
+z = zero
+
+one : Nat
+one = suc zero
+
+add : Nat → Nat → Nat
+add zero y = y
+add (suc x) y = suc (add x y)
+
+fib : Nat → Nat
+fib zero = zero
+fib (suc zero) = suc zero
+fib (suc (suc x)) = add (fib x) (fib (suc x))
+
+fib0 : fib 0 ≡ 0
+fib0 = refl
+
+fib1 : fib 1 ≡ 1
+fib1 = refl
+
+fib2 : fib 2 ≡ 1
+fib2 = refl
+
+fib8 : fib 8 ≡ 21
+fib8 = refl
diff --git a/entries/funemy/z3/z3fib.sh b/entries/funemy/z3/z3fib.sh
new file mode 100755
index 0000000..07ab418
--- /dev/null
+++ b/entries/funemy/z3/z3fib.sh
@@ -0,0 +1,57 @@
+#!/bin/bash
+
+# Instructions:
+#  1. having z3 installed and put under your $PATH
+#  2. making sure z3fib.sh is executable, by `chmod +x z3fib.sh`
+#  3. running as `./z3fib.sh [length of the fib sequence]`
+#  4. having fun :)
+
+if [ -e fib.smt2 ]
+then
+    rm -f fib.smt2
+    touch fib.smt2
+else
+    touch fib.smt2
+fi
+
+if [ "$1" -lt "0" ]; then
+  echo "Argument must be larger than 0."
+  exit 1
+fi
+
+for i in $(seq 0 $1);
+do
+  echo "(declare-const x$i Int)" >> fib.smt2
+done
+
+echo "" >> fib.smt2
+
+echo "(assert" >> fib.smt2
+echo "  (and" >> fib.smt2
+
+for i in $(seq 0 $1);
+do
+  echo "    (>= x$i 0)" >> fib.smt2
+done
+
+echo "    (= x0 0)" >> fib.smt2
+if [ "$1" -ge "1" ]; then
+  echo "    (= x1 1)" >> fib.smt2
+fi
+
+if [ "$1" -ge "2" ]; then
+  for i in $(seq 2 $1);
+  do
+    echo "    (= x$i (+ x$(($i - 2)) x$(($i - 1))))" >> fib.smt2
+  done
+fi
+
+echo "  )" >> fib.smt2
+echo ")" >> fib.smt2
+
+echo "" >> fib.smt2
+
+echo "(check-sat)" >> fib.smt2
+echo "(get-model)" >> fib.smt2
+
+z3 fib.smt2