src/HOL/Datatype_Examples/Lift_BNF.thy

--- a/src/HOL/Datatype_Examples/Lift_BNF.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Datatype_Examples/Lift_BNF.thy	Thu Feb 01 17:06:40 2024 +0100
@@ -104,6 +104,13 @@
 lift_bnf (dead 'k, 'v) fmap [wits: "Map.empty :: 'k \<Rightarrow> 'v option"]
   by auto
 
+class len = fixes len :: "'a \<Rightarrow> nat"
+typedef (overloaded) ('a, 'b :: len) vec = "{xs :: 'a list. length xs = len (undefined :: 'b)}"
+  by (auto intro!: exI[of _ "replicate _ _"])
+setup_lifting type_definition_vec
+lift_bnf (no_warn_wits) ('a, dead 'b :: len) vec
+  by auto
+
 typedef ('a, 'b) tuple_dead = "UNIV :: ('a \<times> 'b) set" ..
 typedef ('a, 'b) tuple_dead1 = "UNIV :: ('a \<times> 'b) set" ..
 typedef ('a, 'b) tuple_dead2 = "UNIV :: ('a \<times> 'b) set" ..