idris-1.3.2: test/docs005/expected

Data type docs005.Foobar : Type
    A foobar with an auto implicit
    
    The function is: public export
Constructors:
    NewFoo : (xs : List String) ->
        (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
        New Foo
        Arguments:
            xs : List String  -- Some xs
            
            ys : List Nat  -- Some ys
            
            (implicit) prf1 : NonEmpty xs  -- A prf
            
            (auto implicit) prf : NonEmpty ys  -- The prf
            
        The function is: public export
docs005.NewFoo : (xs : List String) ->
    (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
    New Foo
    Arguments:
        xs : List String  -- Some xs
        
        ys : List Nat  -- Some ys
        
        (implicit) prf1 : NonEmpty xs  -- A prf
        
        (auto implicit) prf : NonEmpty ys  -- The prf
        
    The function is: Total & public export