| 
						
					 | 
					
						
						
						
						
							
						
						
							fa7e2b5bb6
							
						
					 | 
					
						
						
							
							Add a proof that AboveBelow is a fixed-height lattice (phew!)
						
						
						
						
						
						
						
						Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com> 
						
					 | 
					
						2023-09-18 22:34:58 -07:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					| 
						
					 | 
					
						
						
						
						
							
						
						
							c0db2ccd46
							
						
					 | 
					
						
						
							
							Add a lattice instance for the AboveBelow type
						
						
						
						
						
						
						
						Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com> 
						
					 | 
					
						2023-09-18 20:56:08 -07:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					| 
						
					 | 
					
						
						
						
						
							
						
						
							d338241319
							
						
					 | 
					
						
						
							
							Add a meet operation, too
						
						
						
						
						
						
						
						Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com> 
						
					 | 
					
						2023-09-17 20:01:32 -07:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					| 
						
					 | 
					
						
						
						
						
							
						
						
							03c0b12a3c
							
						
					 | 
					
						
						
							
							Start formalizing the bottom/top lattice
						
						
						
						
						
						
						
						Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com> 
						
					 | 
					
						2023-09-17 19:50:21 -07:00 | 
					
					
						
						
							
							
							
						
					 |