Weird open family stuff

Changes

1 changed files (+27/-0)

• OpenFamily.lean (new)
  • @@ -0,0 +1,27 @@
    + -- https://lean-lang.org/doc/api/Lake/Util/Family.html + + import Lean + import Lake + open Lean + open Lake + + opaque FooFam (idx : Name) : Type + + abbrev FooMap := Std.DTreeMap Name FooFam Name.quickCmp + def FooMap.insert (self : FooMap) (idx : Name) [FamilyOut FooFam idx α] (a : α) : FooMap := + Std.DTreeMap.insert self idx (toFamily a) + def FooMap.get? (self : FooMap) (idx : Name) [FamilyOut FooFam idx α] : Option α := + ofFamily <$> Std.DTreeMap.get? self idx + + family_def bar : FooFam `bar := Nat + family_def baz : FooFam `baz := String + def foo := Id.run do + let mut map : FooMap := {} + map := map.insert `bar 5 + map := map.insert `baz "str" + return map.get? `bar + + def f (idx : Name) [FamilyOut FooFam idx α] := + match + + #eval foo -- 5