Coercions.out « output « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

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

blob: 4b8aa355a13cbe22387276361eb0aa206afc9244 (plain)

P x
     : Prop
R x x
     : Prop
fun (x : foo) (n : nat) => x n
     : foo -> nat -> nat