Put LambdaPi.hs and prelude.lp in a directory of your choice.
$ ghc --make -o lp LambdaPi.hs
[1 of 1] Compiling LP ( LP.hs, LP.o )
Linking lp ...
$ ./lp
Interpreter for lambda-Pi.
Type :? for help.
LP> :?
List of commands: Any command may be abbreviated to :c where
c is the first character in the full name.
evaluate expression
let ` = define variable
assume `` :: assume variable
:type print type of expression
:browse browse names in scope
:load load program from file
:quit exit interpreter
:help, :? display this list of commands
LP> :l prelude.lp
[... lots of type signatures ...]
LP> plus 40 2
42 :: Nat
LP> :t fromto
forall x :: Nat . Vec Nat x
LP> fromto 3
Cons Nat 2 2 (Cons Nat 1 1 (Cons Nat 0 0 (Nil Nat))) :: Vec Nat 3
LP> let v = fromto 3
v :: Vec Nat 3
LP> :t at
forall (x :: *) (y :: Nat) (z :: Vec x y) (a :: Fin y) . x
LP> at Nat 3 v (FSucc 2 (FZero 1))
1 :: Nat
LP> :q
`