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