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