implicits.out « output « test-suite - coq - The formal proof system

about summary refs log tree commit diff

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

blob: 452a90b92c1db0631290569707f6b5a5c1c09735 (plain)

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