lambda_mountain 1.12.9

Lambda Mountain
Documentation 
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


f := λp . (
   (match p (
      ()
      ( () p )
      ( Nil p )
      ( (Variable _) p )
      ( (Literal _) p )
      ( (App( g x )) (
         (App( (f g) (f x) ))
      ))
      ( (Lambda( lhs rhs )) (
         (App( (f lhs) (f rhs) ))
      ))
      ( (prog (GExpr( g ))) (
         ( (f prog) (GExpr (f g)) )
      ))
      ( (prog (Global( n v ))) (
         ( (f prog) (Global( (f n) (f v) )) )
      ))
      ( (prog (Type( tn td ))) (
         ( (f prog) (Type( (f tn) (f td) )) )
      ))
      ( unknown (
         (UnknownTerm unknown)
      ))
   ))
);

main := print-s ( f (() (Global (S V))) );