Specification option

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

specification
   data types 
      Option('a) = Some(. .get : 'a)
                 | None
                 ;
   
   variables 
       a : 'a;
       opt : Option('a);
       get : 'a;
   
   functions 
       . .map ( . ) : Option('a) × ('a → 'b) → Option('b);
       . .getOrElse ( . ) : Option('a) × 'a → 'a;
   
   variables 
       opt : Option('a);
       f : 'a → 'b;
   
   
   axioms 
      map-Some: Some(a).map(f) = Some(f(a));
      used for: s, ls;
      
      map-None: None.map(f) = None;
      used for: s, ls;
      
      getOrElse-Some: Some(a).getOrElse(a0) = a;
      used for: s, ls;
      
      getOrElse-None: None.getOrElse(a0) = a0;
      used for: s, ls;
   
   
end specification