git.iko.soy/Idris-dev
on bb87d4d help sign in
Idris-dev/test/interactive005/expected
34 lines 1.2 kB history raw
1Type checking ./interactive005.idr
23 : Nat
3Hello, World
4main : IO ()
5 This is a docstring
6
7Main.main is Total
8Hello, World
9Prelude.Basics.id : a -> a
10Prelude.Basics.id : {a : Type} -> (__pi_arg : a) -> a
11Prelude.Basics.id : 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 : IO ()
26 This
27 is a
28 docstring
30main : IO ()
31 This is a docstring
33Nat2 : Type
34Invalid filename for compiler output "Test.idr"