Syntax highlighting tests

syntax-highlighting-tests.idr

module Main

import Data.Vect

main : IO ()
main = putStrLn "Hello world\n\o44\5\xa4"

zipWithF : (a -> b -> c) -> List a -> List b -> List c
zipWithF f xs ys = ?zipWithF_rhs_2

add : Nat -> Nat -> Nat
add a b = a + b

c : Nat
c = 5

ch : Char
ch = 'c'

octChar : Char
octChar = '\o4'

data Answer = Yes | No

reverse : List a -> List a
reverse xs = revAcc [] xs where
    revAcc : List a -> List a -> List a
    revAcc acc [] = acc
    revAcc acc (x :: xs) = revAcc (x :: acc) xs

apply : (a -> b) -> a -> b
apply f x = f x

added4And5 : Nat
added4And5 = 4 `add` 5

data Vect1 : Nat -> Type -> Type where
    Nil  : Vect1 Z a
    (::) : a -> Vect1 k a -> Vect1 (S k) a

app : Vect n a -> Vect m a -> Vect (n + m) a
app {n=Z}   []        ys = ys
app {n=S k} (x :: xs) ys = x :: xs ++ ys

||| Use this typeclass to debug some code
class Debug a where
    debug : a -> String

instance Debug Nat where
    debug Z = "Z"
    debug (S k) = "s" ++ show k