lsts 0.6.34

Large Scale Type Systems
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
31
32
33
34
35
36
37
38
39
40
41

use lsts::tlc::TLC;

#[test]
fn parse_simplytyped() {
   let mut tlc = TLC::new();
   tlc.parse_str(None,"a;").unwrap();
   tlc.parse_str(None,"a();").unwrap();
   tlc.parse_str(None,"a(b);").unwrap();
   tlc.parse_str(None,"a(b,c);").unwrap();
   tlc.parse_str(None,"a.f;").unwrap();
   tlc.parse_str(None,"a.f(b);").unwrap();
   tlc.parse_str(None,"a.f(b,c);").unwrap();
   tlc.parse_str(None,"let t: ?;").unwrap();
   tlc.parse_str(None,"let t: T;").unwrap();
   tlc.parse_str(None,"let t: T?;").unwrap();
   tlc.parse_str(None,"let t: ();").unwrap();
   tlc.parse_str(None,"let t: (A);").unwrap();
   tlc.parse_str(None,"let t: (A,B);").unwrap();
   tlc.parse_str(None,"let t: T<A,B>;").unwrap();
   tlc.parse_str(None,"let t: ()->A;").unwrap();
   tlc.parse_str(None,"let t: A->B;").unwrap();
   tlc.parse_str(None,"let t: (A)->B;").unwrap();
   tlc.parse_str(None,"let t: (A,B)->C;").unwrap();
   tlc.parse_str(None,"let a: A; let a: B;").unwrap();
   tlc.parse_str(None,"let a: A; let b: A;").unwrap();
   tlc.parse_str(None,"let f();").unwrap();
   tlc.parse_str(None,"let f(a:A);").unwrap();
   tlc.parse_str(None,"let f(a:A,b:B);").unwrap();
   tlc.parse_str(None,"let f(a:A);").unwrap();
   tlc.parse_str(None,"let f(a:A::Term);").unwrap();
   tlc.parse_str(None,"let f():A;").unwrap();
   tlc.parse_str(None,"let f()::Term;").unwrap();
   tlc.parse_str(None,"a `f` b;").unwrap();
   tlc.parse_str(None,"type A;").unwrap();
   tlc.parse_str(None,"forall :A,:B::C. (A,B);").unwrap();
   tlc.parse_str(None,"forall :A,:B::C. (A,B) :: R;").unwrap();
   tlc.parse_str(None,"{a; b;};").unwrap();

   //Type Names, like Ab, are always valid constants, even without a prelude
   tlc.parse_str(None,"let t: T[Ab];").unwrap();
}