ブログ記事用の例

environment.v

Section s1.

Axiom a : nat.
Variable b : nat.

Definition c : nat := 1.
Let d : nat := 1.

Print All.

Definition e : nat := a+b+c+d.
Print e.

End s1.

Print All.
Print e.

example.v

Definition K : forall (P Q : Prop), P -> Q -> P.
Proof.
  Show Proof.
  intros.
  Show Proof.
  assumption.
  Show Proof.
Qed.
Print K.
Definition K' : forall (P Q : Prop), P -> Q -> P :=
  fun (P Q : Prop) (H : P) (_ : Q) => H.
Check K'.

Goal forall (P Q : Prop), P -> Q -> P /\ Q.
Proof.
  intros.
  split.
  Show Proof.
Abort.