cryptol/tests/mono-binds/test05.icry.stdout

Loading module Cryptol
Loading module Cryptol
Loading module test05
[warning] at ./test05.cry:9:3--9:6
    This binding for foo shadows the existing binding from
    (at ./test05.cry:4:1--4:4, foo)
[warning] at ./test05.cry:13:5--13:8
    This binding for foo shadows the existing binding from
    (at ./test05.cry:9:3--9:6, foo)
module test05
import Cryptol
/* Not recursive */
test05::foo : [10]
test05::foo = Cryptol::demote 10 [10] <>

/* Not recursive */
test05::test : {n, a, b} (Zero a, Literal 10 b) => [n]a -> b
test05::test = \{n, a, b} (Zero a, Literal 10 b) (a : [n]a) ->
               Cryptol::demote 10 b <>
               where
                 /* Not recursive */
                 test05::foo : [10]
                 test05::foo = Cryptol::demote 10 [10] <>
                 
                 /* Not recursive */
                 test05::f : {m} (fin m) => [n + m]a
                 test05::f = \{m} (fin m) ->
                             test05::bar m <>
                             where
                               /* Not recursive */
                               test05::foo : [n]a
                               test05::foo = a
                               
                               /* Not recursive */
                               test05::bar : {i} (fin i) => [i + n]a
                               test05::bar = \{i} (fin i) ->
                                             (Cryptol::#) i n a <> (Cryptol::zero ([i]a) <>) test05::foo
                               
                             
                 
               

Loading module Cryptol
Loading module test05
[warning] at ./test05.cry:9:3--9:6
    This binding for foo shadows the existing binding from
    (at ./test05.cry:4:1--4:4, foo)
[warning] at ./test05.cry:13:5--13:8
    This binding for foo shadows the existing binding from
    (at ./test05.cry:9:3--9:6, foo)
[warning] at ./test05.cry:14:11--14:21:
  Defaulting type argument 'front' of '(#)' to 0
module test05
import Cryptol
/* Not recursive */
test05::foo : [10]
test05::foo = Cryptol::demote 10 [10] <>

/* Not recursive */
test05::test : {n, a, b} (Zero a, Literal 10 b) => [n]a -> b
test05::test = \{n, a, b} (Zero a, Literal 10 b) (a : [n]a) ->
               Cryptol::demote 10 b <>
               where
                 /* Not recursive */
                 test05::foo : [10]
                 test05::foo = Cryptol::demote 10 [10] <>
                 
                 /* Not recursive */
                 test05::f : [n]a
                 test05::f = test05::bar
                             where
                               /* Not recursive */
                               test05::foo : [n]a
                               test05::foo = a
                               
                               /* Not recursive */
                               test05::bar : [n]a
                               test05::bar = (Cryptol::#) 0 n a <> (Cryptol::zero ([0]a) <>) test05::foo