remove WIP lines on equivalence proof

Qpf/Elab/ShapeType.lean

@@ -197,97 +197,3 @@ def addToEnvironmentAsPFunctor (s : ShapeType n) : TermElabM Name := do
   }
   addAndCompile decl
   return name
-
-/-!
-## Equivalence proof
--/
-
-section Tactic
-open Tactic
-
-def generateBox (s : ShapeType n) : TermElabM Unit := do
-  let ty := (Name.anonymous, .implicit, fun _ => pure <| Expr.sort s.univ.succ)
-  let tys := Array.range n |>.map fun _ => ty
-
-  withLocalDecls tys <| fun params => do
-
-  let Shape := mkAppN (Expr.const s.name s.levelParams) params
-  withLocalDeclD .anonymous Shape <| fun sVar => do
-
-    let paramsVec := sorry /- `params` as a TypeVec -/
-    let PObj := mkApp (.const ``MvPFunctor.Obj [0]) (.const (.str s.name PFunctorSuffix) [])
-
-    let casesOn := mkAppN (.const (.str s.name "casesOn") s.levelParams) params
-    let motive  := mkLambda .anonymous .default (← mkFreshExprMVar none)
-                    (mkApp PObj paramsVec)
-    let casesOn := mkApp casesOn motive
-/-
-open TypeVec (appendFun) in
-def Shape.box : Shape α β → Shape._PFunctor.Obj ((Fin2.elim0 ::: α) ::: β) :=
-  fun s =>
-  @Shape.casesOn α β (fun _ => Shape._PFunctor.Obj ((Fin2.elim0 ::: α) ::: β))
-    s
-    (fun a b c => Sigma.mk (0 : Fin 2) <|
-      appendFun (appendFun Fin2.elim0
-        (Fin.cons c Fin.elim0))
-        (Fin.cons a <| Fin.cons b Fin.elim0)
-    )
-    (fun a => Sigma.mk (1 : Fin 2) <|
-      appendFun (appendFun Fin2.elim0 (Fin.cons a Fin.elim0)) (Fin.elim0)
-    ) -/
-
-/-- Prove the equivalence between the inductive and pfunctor definitions of a
-specific shape type.
-
-NOTE: this definition assumes you've already added both definitions to the
-environment, through calling `add`
- -/
-def proveInductiveEquivPFunctor (s : Name) : TacticM Expr := do
-  let originalGoals ← getGoals
-
-  -- stop
-  -- let sInfo ← getConstInfoInduct s
-  -- sInfo.toConstantVal
-  -- let sE := mkConst
-
-  sorry
-
-/-
-## Scratch space
--/
-
-inductive Foo (α β : Type u) : Type u
-  -- | foo : α → β → α → Foo α β
-
-#check InductiveVal
-
-#eval @id (MetaM _) <| do
-  let .inductInfo info ← getConstInfo ``Foo
-    | return ()
-  println! "type: {info.type}"
-  println! "params: {info.numParams}"
-
-set_option trace.QPF true
-def shape : ShapeType 2 where
-  name := `Shape
-  univ := 0
-  params := [`α, `β]
-  ctors := [
-    {
-      name := `Shape.foo
-      args := [⟨`x, 1⟩, ⟨`y, 1⟩, ⟨.anonymous, 0⟩]
-    },
-    {
-      name := `Shape.bar
-      args := [⟨`x, 0⟩]
-    }
-  ]
-
-#eval shape.addToEnvironmentAsInductive
-#eval shape.addToEnvironmentAsPFunctor
-
-#check Shape.foo
-#print Shape._PFunctor
-#print Shape
-
-#check Shape.rec