git.iko.soy/Idris-dev
on cf47310 help sign in
Idris-dev/test/interactive005/expected
36 lines 1.2 kB history raw
13 : Nat
2Hello, World
3Main.main : IO ()
4 This is a docstring
5
6 The function is Total
7Main.main is Total
8Hello, World
9id : a -> a
10Prelude.Basics.id : {a : Type} -> a -> a
11id : a -> a
13 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY
14 EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
15 IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
16 PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE
17 LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
18 CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
19 SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
20 BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
21 WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
22 OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN
23 IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
25Main.main : IO ()
26 This
27 is a
28 docstring
30 The function is Total
31Main.main : IO ()
32 This is a docstring
34 The function is Total
35Nat2 : Type
36Invalid filename for compiler output "Test.idr"