From 8c3619fcb5e01b14eeab69bfa8c88cd75ed16ac9 Mon Sep 17 00:00:00 2001
From: braxtonhall
Date: Sun, 23 Oct 2022 16:28:11 -0700
Subject: Make Jon's work/description consistent with everyone else

---
 entries/ionathanch/agda/Fib.agda | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 entries/ionathanch/agda/Fib.agda

(limited to 'entries/ionathanch')

diff --git a/entries/ionathanch/agda/Fib.agda b/entries/ionathanch/agda/Fib.agda
new file mode 100644
index 0000000..a12b0a5
--- /dev/null
+++ b/entries/ionathanch/agda/Fib.agda
@@ -0,0 +1,19 @@
+
+open import Agda.Builtin.Nat
+open import Agda.Builtin.List
+open import Agda.Builtin.Reflection
+
+data Fib : Nat → Nat → Set where
+  instance F0 : Fib 0 0
+  instance F1 : Fib 1 1
+  instance Fk : ∀ {k n m} → ⦃ Fib k n ⦄ → ⦃ Fib (suc k) m ⦄ → Fib (suc (suc k)) (n + m)
+
+fib' : ∀ k {n} → ⦃ Fib k n ⦄ → Nat
+fib' k {n} ⦃ fib ⦄ = n
+
+macro
+  fib : Term → Term → TC _
+  fib t hole = unify hole (def (quote fib') (arg i t ∷ []))
+    where i = arg-info visible (modality relevant quantity-ω)
+
+{- Get the [n]th Fibonacci number by normalization via C-n `fib [n]`. -}
-- 
cgit v1.2.3-70-g09d2


From 4c717196fd630c5c207e114ffa9ca9c301eb1198 Mon Sep 17 00:00:00 2001
From: Jonathan Chan
Date: Sun, 23 Oct 2022 23:07:43 -0400
Subject: Fortran :) (also moved my Agda file up a dir)

---
 README.md                        |  3 ++-
 entries/ionathanch/Fib.agda      | 19 +++++++++++++++++++
 entries/ionathanch/agda/Fib.agda | 19 -------------------
 entries/ionathanch/fib.f90       | 21 +++++++++++++++++++++
 4 files changed, 42 insertions(+), 20 deletions(-)
 create mode 100644 entries/ionathanch/Fib.agda
 delete mode 100644 entries/ionathanch/agda/Fib.agda
 create mode 100644 entries/ionathanch/fib.f90

(limited to 'entries/ionathanch')

diff --git a/README.md b/README.md
index 51ade8f..0fcbc53 100644
--- a/README.md
+++ b/README.md
@@ -16,7 +16,8 @@ For a submission to the upcoming "Reclaim your space" exhibition at [Hatch Art G
 <!-- - `imperitive-church` imperitive implementation in the lambda calculus -->
 
 ### [`ionathanch`](https://github.com/ionathanch)
-- [`agda`](./entries/ionathanch/agda/Fib.agda)
+- [`agda`](./entries/ionathanch/Fib.agda)
+- [`fortran`](./entries/ionathanch/fib.f90)
 
 ### [`funemy`](https://github.com/funemy)
 - [`agda`](./entries/funemy/agda/fib1.agda)
diff --git a/entries/ionathanch/Fib.agda b/entries/ionathanch/Fib.agda
new file mode 100644
index 0000000..a12b0a5
--- /dev/null
+++ b/entries/ionathanch/Fib.agda
@@ -0,0 +1,19 @@
+
+open import Agda.Builtin.Nat
+open import Agda.Builtin.List
+open import Agda.Builtin.Reflection
+
+data Fib : Nat → Nat → Set where
+  instance F0 : Fib 0 0
+  instance F1 : Fib 1 1
+  instance Fk : ∀ {k n m} → ⦃ Fib k n ⦄ → ⦃ Fib (suc k) m ⦄ → Fib (suc (suc k)) (n + m)
+
+fib' : ∀ k {n} → ⦃ Fib k n ⦄ → Nat
+fib' k {n} ⦃ fib ⦄ = n
+
+macro
+  fib : Term → Term → TC _
+  fib t hole = unify hole (def (quote fib') (arg i t ∷ []))
+    where i = arg-info visible (modality relevant quantity-ω)
+
+{- Get the [n]th Fibonacci number by normalization via C-n `fib [n]`. -}
diff --git a/entries/ionathanch/agda/Fib.agda b/entries/ionathanch/agda/Fib.agda
deleted file mode 100644
index a12b0a5..0000000
--- a/entries/ionathanch/agda/Fib.agda
+++ /dev/null
@@ -1,19 +0,0 @@
-
-open import Agda.Builtin.Nat
-open import Agda.Builtin.List
-open import Agda.Builtin.Reflection
-
-data Fib : Nat → Nat → Set where
-  instance F0 : Fib 0 0
-  instance F1 : Fib 1 1
-  instance Fk : ∀ {k n m} → ⦃ Fib k n ⦄ → ⦃ Fib (suc k) m ⦄ → Fib (suc (suc k)) (n + m)
-
-fib' : ∀ k {n} → ⦃ Fib k n ⦄ → Nat
-fib' k {n} ⦃ fib ⦄ = n
-
-macro
-  fib : Term → Term → TC _
-  fib t hole = unify hole (def (quote fib') (arg i t ∷ []))
-    where i = arg-info visible (modality relevant quantity-ω)
-
-{- Get the [n]th Fibonacci number by normalization via C-n `fib [n]`. -}
diff --git a/entries/ionathanch/fib.f90 b/entries/ionathanch/fib.f90
new file mode 100644
index 0000000..3cf1850
--- /dev/null
+++ b/entries/ionathanch/fib.f90
@@ -0,0 +1,21 @@
+PROGRAM main
+  ! The 93rd Fibonacci number is the largest that fits in 64 bits anyway
+  CHARACTER(3) :: kth
+  INTEGER :: k
+  CALL get_command_argument(1, kth)
+  READ(kth, *) k
+  WRITE(*, *) fib(k)
+CONTAINS
+
+PURE RECURSIVE INTEGER*8 FUNCTION fib(k) RESULT(n)
+  INTEGER, INTENT (IN) :: k
+  IF (k == 0) THEN
+    n = 0
+  ELSE IF (k == 1) THEN
+    n = 1
+  ELSE
+    n = fib(k - 1) + fib(k - 2)
+  END IF
+END FUNCTION fib
+
+END PROGRAM
-- 
cgit v1.2.3-70-g09d2