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

summary refs log tree commit diff

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

blob: e4837199fe191ab72e158b1521a4d811c35b6e0e (plain)

(compose 3!nat S)
     : (nat->nat)->nat->nat
(ex_intro 2![_:nat]True 3!(0) I)
     : (ex [_:nat]True)