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

about summary refs log tree commit diff homepage

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

blob: c1a7e961a9be28d01c410fd517e94cec706fb4ae (plain)

2 3
     : PAIR
2[+]3
     : nat
forall (A : Set) (le : A -> A -> Prop) (x y : A), le x y \/ le y x
     : Prop