math-comp

Mathematical Components library for the Coq proof assistant

brewmacoslinux

Try with needOr install directly

About

Mathematical Components for the Coq proof assistant

coqccoqtop

Compile a Coq file using Mathematical Components$ coqc -R $(brew --prefix math-comp)/lib/coq/user-contrib/mathcomp mathcomp myproof.v

Start interactive Coq session with Mathematical Components loaded$ coqtop -R $(brew --prefix math-comp)/lib/coq/user-contrib/mathcomp mathcomp

Check Mathematical Components library installation path$ brew --prefix math-comp