From e044dc9b578bd6d1e2da515b4269db063859a217 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 18 Dec 2024 13:33:06 +0000
Subject: [PATCH] cleanup

---
 Qpf/Elab/ShapeType.lean | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/Qpf/Elab/ShapeType.lean b/Qpf/Elab/ShapeType.lean
index 182b1ce..2933c44 100644
--- a/Qpf/Elab/ShapeType.lean
+++ b/Qpf/Elab/ShapeType.lean
@@ -123,18 +123,6 @@ def addToEnvironmentAsInductive (s : ShapeType n) : TermElabM Unit := do
 ## Defining a shape type as a polynomial functor
 -/
 
-#check MvPFunctor.mk
-
--- set_option pp.universes true in
-#check Fin.cons (n:=?m) (α := fun _ => TypeVec n)
-#check Fin.elim0 (α := TypeVec n)
-
-#check Fin.cons
-
-set_option pp.universes true in
-#check TypeVec.append1
-#check MvPFunctor
-
 /-- Convert an array of expressions of type `Type $u` into a single expression
 of type `TypeVec.{$u}` -/
 def arrayToTypeVecExpr (x : Array Expr) (u : Level) : Expr :=