Tree/Map/HashMap in Inductive Data Type

Stream: lean4

[Atticus Kuhn]

I'm trying to put a tree/dictionary/hashmap in an inductive data type

import Std

inductive T : Type where
  | c : Std.TreeMap Int T → T

I get the confusing error:

test.lean:3:0
(kernel) application type mismatch
  Std.DTreeMap.Internal.Impl.WF inner
argument has type
  _nested.Std.DTreeMap.Internal.Impl_3
but function has type
  (Std.DTreeMap.Internal.Impl Int fun x ↦ T) → Prop

What does this error mean? Where do these internal symbols come from? Can I put a tree/map/hashmap in an inductive data structure?

[Aaron Liu]

from docs#Std.DHashMap:

These hash maps contain a bundled well-formedness invariant, which means that they cannot be used in nested inductive types. For these use cases, Std.DHashMap.Raw and Std.DHashMap.Raw.WF unbundle the invariant from the hash map. When in doubt, prefer DHashMap over DHashMap.Raw.

[Atticus Kuhn]

Thank you, using Std.TreeMap.Raw solved the issue.

[Jovan Gerbscheid]

A quote from the year 3 roadmap of the FRO:

Nesting induction through collections such as HashMap and TreeMap will be supported.