sdfsd.idr

-- We use TTImp instead of Name because in name quotation on primtypes `{{Int}}
-- is not parsed as a name, in fact prims are specifically excluded from this.
||| newtype "Foo" `(Int) ~~> data Foo : Type where MkFoo : Int -> Foo
newtype : String -> Visibility -> TTImp -> Elab ()
newtype name0 vis ty = do
    name <- inCurrentNS (UN name0)
    let con = MkTy eFC (mapName ("Mk" ++) name) `(~ty -> ~(IVar eFC name))
    let decl = IData eFC vis $ MkData eFC name (IType eFC) [] [con]
    declare [decl]

export
data FooPtr : Type where

data Fraf : Nat -> Type where
  Geb : Fraf Z

%runElab newtype "Foo1" Private `(Int) -- is a primtype
%runElab newtype "Foo2" Private `(FooPtr) -- has no cons
-- %runElab newtype "Foo3" Private `(Fraf) -- needs params, not handled yet

caseFoo1 : Foo1 -> Int
caseFoo1 (MkFoo1 x) = x

caseFoo2 : Foo2 -> FooPtr
caseFoo2 (MkFoo2 x) = x