CODEWITHSUNDEEP
syntaxcoq
Olle Härstedt
Olle Härstedt

Reputation: 4020

Coq intros syntax

Could someone please explain the intros syntax below?

Lemma is_single_nBTP : forall t, is_single_nBT t = true -> exists n : nat, t = Leaf n.
Proof.
intros [ nleaf | nnode t1 t2] h.
exists nleaf.
reflexivity.
...

Where nBT is a nat binary tree, and is_single_nBT is a function which returns true when t is a leaf.

(This example is from this lecture.)

Upvotes: 3

Views: 709

Answers (1)

Philip JF
Philip JF

Reputation: 28539

The [A | B] is a disjunction pattern. It is the same idea as case analysis in functional programming languages.

In this case you are creating two subgoals. One where t is known to be a leaf with the natural number nleaf as its argument, and another where t is introduced as a Node with the arguments nnode, t1, and t2.

Either way another argument h : is_single_nBT ? = true is introduced where ? is either Leaf nleaf or Node nnode t1 t2.

Upvotes: 4

Related Questions