[ tests ] Add tests for :doc for records and single-constructor type

This commit is contained in:
Johann Rudloff 2021-05-05 22:54:04 +02:00 committed by G. Allais
parent d8891bf7b9
commit 4b7d85653a
3 changed files with 26 additions and 1 deletions

View File

@ -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

View File

@ -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!

View File

@ -1,3 +1,5 @@
:browse Doc
:doc Foo
:doc WrappedInt
:doc SimpleRec
:q