3 : Nat
Hello, World
Main.main : IO ()
    This is a docstring
    
    The function is Total
Main.main is Total
Hello, World
id : a -> a
Prelude.Basics.id : {a : Type} -> a -> a
id : a -> a

	 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY  
	 EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE     
	 IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR    
	 PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE   
	 LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR   
	 CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF  
	 SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR       
	 BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, 
	 WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE  
	 OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN
	 IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

Main.main : IO ()
    This
    is a
    docstring
    
    The function is Total
Main.main : IO ()
    This is a docstring
    
    The function is Total
Nat2 : Type
Invalid filename for compiler output "Test.idr"