tests/test-polyrec.why

   1
   2
   3 theory T
   4
   5 use option.Option
   6
   7 type t 'a = A | Lam (t (option 'a))
   8
   9 inductive r (t 'a) (t 'a) =
  10  | cas : forall x y:t (option 'a). r x y -> r (Lam x) (Lam y)
  11
  12 goal G : true
  13
  14 end