File tree Expand file tree Collapse file tree 1 file changed +58
-0
lines changed Expand file tree Collapse file tree 1 file changed +58
-0
lines changed Original file line number Diff line number Diff line change 1+ (new-declaration (spec X Y) (:= X Y))
2+ (new-declaration (:: Tested Test)
3+   (== @(interact #Tested #Test) ok))
4+ 
5+ ' test of linear identity
6+ (spec (larrow a a) {
7+   [+testrl [
8+     [-1 -2 +c5]
9+     [-3] [-4 +c6]
10+     [-c5 +7] [-c6]
11+     @[-7 ok]]]
12+   [+testrr [
13+     [-1 -2 +c5]
14+     [-3] [-4 +c6]
15+     [-c5] [+7 -c6]
16+     @[-7 ok]]]
17+   [+testll [
18+     [-1 -2 +c5]
19+     [-4] [-3 +c6]
20+     [-c5 +7] [-c6]
21+     @[-7 ok]]]
22+   [+testlr [
23+     [-1 -2 +c5]
24+     [-4] [-3 +c6]
25+     [-c5] [+7 -c6]
26+     @[-7 ok]]]})
27+ 
28+ (:= id { [+1 +3] [+2 +4]})
29+ 'TODO (:: id (larrow a a))
30+ 
31+ 'cut-elimination
32+ (:= ps1 {
33+   [+vehicle [
34+     [+1 +2]
35+     @[3 +4]
36+     [+5 6]
37+   ]]
38+   [+cuts [
39+     [-1 -4]
40+     [-2 -5]
41+   ]]
42+ })
43+ 
44+ (:= vehicle (eval (interact #ps1 @[-vehicle])))
45+ (:= cuts    (eval (interact #ps1 @[-cuts])))
46+ 
47+ (show (interact #vehicle #cuts))
48+ 
49+ (spec (tens a b) {
50+   [-1 -2 +3]
51+   @[-3 ok]})
52+ 
53+ (new-declaration (::lin Tested Test)
54+   (== @(fire #Tested #Test) ok))
55+ 
56+ (:= vehicle [+1 +2])
57+ ' does not typecheck
58+ ' (::lin vehicle (tens a a)
 
 
   
 
     
   
   
          
    
    
     
    
      
     
     
    You can’t perform that action at this time.
  
 
    
  
    
      
        
     
       
      
     
   
 
    
    
  
 
  
 
     
    
0 commit comments