UnivBinders.out « output « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/output/UnivBinders.out

blob: 128bc7767361aa8d060fadbb12ea619ec2d0107b (plain)

bar@{u} = nat
     : Wrap@{u} Set
(* u |= Set < u
         *)

bar is universe polymorphic