cryptol/tests/regression/specialize.icry.stdout

Loading module Cryptol
Loading module Cryptol
Loading module specialize
Expression type:
(Bit, Bit) -> (Bit, Bit)
Original expression:
specialize::top
Specialized expression:
specialize::top
where
  /* Not recursive */
  specialize::f : (Bit, Bit) -> (Bit, Bit)
  specialize::f = \ (__p1 : (Bit, Bit)) ->
                  (specialize::x, specialize::y)
                  where
                    /* Not recursive */
                    specialize::x : Bit
                    specialize::x = __p1 .0 /* of 2 */
                    
                    /* Not recursive */
                    specialize::y : Bit
                    specialize::y = __p1 .1 /* of 2 */
                    
                  
  
  /* Not recursive */
  specialize::top : (Bit, Bit) -> (Bit, Bit)
  specialize::top = \ (__p0 : (Bit, Bit)) ->
                    specialize::f (specialize::x, specialize::y)
                    where
                      /* Not recursive */
                      specialize::x : Bit
                      specialize::x = __p0 .0 /* of 2 */
                      
                      /* Not recursive */
                      specialize::y : Bit
                      specialize::y = __p0 .1 /* of 2 */