From 87c73ed2b6e2158e897b6d48d64df020a3c3d3d1 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 18 Dec 2024 13:37:35 +0000 Subject: [PATCH] add a not on what is(n't) implemented --- Qpf/Elab/ShapeType.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Qpf/Elab/ShapeType.lean b/Qpf/Elab/ShapeType.lean index 2933c44..000dd5b 100644 --- a/Qpf/Elab/ShapeType.lean +++ b/Qpf/Elab/ShapeType.lean @@ -17,6 +17,11 @@ A shape type is an inductive type where Note that this implies that shape types are non-recursive! +This file is still under active development, currently we've implemented +definitions of a shape type as both `inductive`s and `PFunctor`s, but +are still lacking suppport for automatically deriving the equivalence between +these definitions, and the subsequent `MvQPF` instance for the `inductive` +version. -/ open Qq