| 
                definition:  | 
              
              
                banner :: String banner = unlines [bannerLine, bannerText, bannerLine] where bannerText = "Contract Checking/Verification Tool (Version of 26/10/24)" bannerLine = take (length bannerText) (repeat '=')  | 
              
            
| 
                demand:  | 
              
              
                no demanded arguments  | 
              
            
| 
                deterministic:  | 
              
              
                deterministic operation  | 
              
            
| 
                failfree:  | 
              
              
                ()  | 
              
            
| 
                indeterministic:  | 
              
              
                referentially transparent operation  | 
              
            
| 
                infix:  | 
              
              
                no fixity defined  | 
              
            
| 
                iotype:  | 
              
              
                 {() |-> _}
               | 
              
            
| 
                name:  | 
              
              
                banner  | 
              
            
| 
                precedence:  | 
              
              
                no precedence defined  | 
              
            
| 
                result-values:  | 
              
              
                _  | 
              
            
| 
                signature:  | 
              
              
                String  | 
              
            
| 
                solution-complete:  | 
              
              
                operation might suspend on free variables  | 
              
            
| 
                terminating:  | 
              
              
                possibly non-terminating  | 
              
            
| 
                totally-defined:  | 
              
              
                reducible on all ground data terms  |