Loading module Cryptol
Loading module Cryptol
Loading module test04
module test04
import Cryptol
/* Not recursive */
test04::test : {a, b} (Literal 10 b) => a -> ((a, ()), (a, b))
test04::test = \{a, b} (Literal 10 b) (a : a) ->
               (test04::f () (), test04::f b (Cryptol::demote 10 b <>))
               where
                 /* Not recursive */
                 test04::f : {c} c -> (a, c)
                 test04::f = \{c} (x : c) -> (a, x)
                 
               

Loading module Cryptol
Loading module test04

[error] at ./test04.cry:3:19--3:21:
  Unsolved constraints:
    Literal 10 ()
      arising from
      use of literal or demoted expression
      at ./test04.cry:3:19--3:21