-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathLambdaPi-README
40 lines (33 loc) · 1.02 KB
/
LambdaPi-README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
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.
<expr> evaluate expression
let <var> = <expr> define variable
assume <var> :: <expr> assume variable
:type <expr> print type of expression
:browse browse names in scope
:load <file> 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