cleanup

alexkeizer · Dec 18, 2024 · e044dc9 · e044dc9
1 parent 3cb8458
commit e044dc9
Showing 1 changed file with 0 additions and 12 deletions.
diff --git 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 :=