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