git.iko.soy/Idris-dev
on bb6bba2 help sign in
Idris-dev/src/Main.hs
15 lines 318 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 let OK ctxt = checkProgram [] defs
14 print ctxt
15 runShell (initState ctxt)