git.iko.soy/Idris-dev
on cbc60eb help sign in
Idris-dev/src/Main.hs
17 lines 414 B history raw
1module Main where
3import CoreParser
4import ShellParser
5import Core
6import Typecheck
7import ProofState
8import ProofShell
10main = do f <- readFile "test.mi"
11 let Right defs = parseFile f
12 print defs
13 case checkProgram [] defs of
14 OK ctxt -> do print ctxt
15 runShell (initState ctxt)
16 return ()
17 err -> print err