README.md

Coq

prerequisite

brew install coq

Coq Commands

coqc prime.v
# will produce prime.vo

coqtop
# see https://coq.inria.fr/refman/proof-engine/vernacular-commands.html
Coq < Require Import prime.

Coq < Print plus.
plus = fun n m : nat => n + m
     : nat -> nat -> nat

Arguments plus (_ _)%nat_scope
Coq < Eval compute in plus 1 2.
     = 3
     : nat

references

• プログラミング Coq
• Introduction and Contents