From cdc833b1e8cc29e192cfccef07e29ac442c3e562 Mon Sep 17 00:00:00 2001
From: eyihluyc <theviolthevioletandthewine@gmail.com>
Date: Thu, 8 Feb 2024 00:21:35 -0500
Subject: [PATCH] Delete demo of `nf` and `whnf`

---
 Minimal/Test.lean | 37 -------------------------------------
 1 file changed, 37 deletions(-)
 delete mode 100644 Minimal/Test.lean

diff --git a/Minimal/Test.lean b/Minimal/Test.lean
deleted file mode 100644
index a961f80a..00000000
--- a/Minimal/Test.lean
+++ /dev/null
@@ -1,37 +0,0 @@
-import Minimal.calculus
-
-set_option autoImplicit false
-
-open OptionalAttr
-open Term
-
-
-mutual
-partial def termToString : Term → String
-  | Term.loc n => s!"ρ{n}"
-  | Term.dot t s => s!"{termToString t}.{s}"
-  | Term.app t a u => s!"{termToString t}({a} ↦ {termToString u})"
-  | Term.obj o =>
-    "〚" ++ listToString o ++ "〛"
-
-partial def listToString : List (Attr × OptionalAttr) → String
-      | [] => ""
-      | [(a, t)] => s!"{a} ↦ {attrToString t}"
-      | List.cons (a, t) l => s!"{a} ↦ {attrToString t}, " ++ (listToString l)
-
-partial def attrToString : OptionalAttr → String
-  | attached x => termToString x
-  | void => "∅"
-end
-
-
-instance : ToString OptionalAttr where
-  toString := attrToString
-
-instance : ToString Term where
-  toString := termToString
-
-
-#eval whnf (app (dot (obj [("x", attached (obj [("y", void)]))]) "x") "y" (dot (obj [("z", attached (loc 3)), ("w", void)]) "z"))
-
-#eval nf (app (dot (obj [("x", attached (obj [("y", void)]))]) "x") "y" (dot (obj [("z", attached (loc 3)), ("w", void)]) "z"))