ToU.idr

ToU.idr

module Infer

data Foo : (xs : List (String, Type)) -> Type where
  MkFoo : Foo xs

mkFoo : {xs : List (String, Type)} -> Foo xs
mkFoo = MkFoo

foo : ?  -- Foo ?xs
foo = mkFoo {xs = [("Foo", Int), ("Bar", Nat)]}

data Bar : (xs : List String) -> Type where
  MkBar : Bar xs

mkBar : {xs : List String} -> Bar xs
mkBar = MkBar

bar : ?
bar = mkBar {xs = ["Foo", "Bar"]}