diff --git a/tests/idris2/docs002/Doc.idr b/tests/idris2/docs002/Doc.idr index 74b7fe7a2..29584c89c 100644 --- a/tests/idris2/docs002/Doc.idr +++ b/tests/idris2/docs002/Doc.idr @@ -13,6 +13,16 @@ export hello : Int -> Int hello x = x*2 +public export +data WrappedInt : Type where + MkWrappedInt : Int -> WrappedInt + +public export +record SimpleRec where + constructor MkSimpleRec + a : Int + b : String + namespace NS namespace NestedNS diff --git a/tests/idris2/docs002/expected b/tests/idris2/docs002/expected index 9d6ba75c6..7c4af7daf 100644 --- a/tests/idris2/docs002/expected +++ b/tests/idris2/docs002/expected @@ -1,9 +1,22 @@ 1/1: Building Doc (Doc.idr) -Doc> hello : Int -> Int +Doc> MkSimpleRec : Int -> String -> SimpleRec +MkWrappedInt : Int -> WrappedInt +SimpleRec : Type +WrappedInt : Type +a : SimpleRec -> Int +b : SimpleRec -> String +hello : Int -> Int Hello! world : Nat -> Nat World! Doc> Doc.NS.NestedNS.Foo : Type A type of Foo +Doc> Doc.WrappedInt : Type + Totality: total + Constructor: MkWrappedInt : Int -> WrappedInt + +Doc> Doc.SimpleRec : Type + Totality: total + Constructor: MkSimpleRec : Int -> String -> SimpleRec Doc> Bye for now! diff --git a/tests/idris2/docs002/input b/tests/idris2/docs002/input index eaab24bfc..551d81cc5 100644 --- a/tests/idris2/docs002/input +++ b/tests/idris2/docs002/input @@ -1,3 +1,5 @@ :browse Doc :doc Foo +:doc WrappedInt +:doc SimpleRec :q