search

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
199 stars 50 forks source link

Clarify instructions in Introduction.v #139

Closed rtlevy closed 5 years ago

rtlevy commented 5 years ago

Several of the lemmas in tutorial/Introduction.v require the use of the setoid_rewrite tactic in order to rewrite expressions under binders. This first occurs in the proof of interp_write_one. Users of the tutorial with a basic Coq background will not necessarily have encountered setoid_rewrite and are likely to get stuck on the proofs which require it.

This PR adds a few sentences to Introduction.v in order to explain that setoid_rewrite must be used in these cases.

Lysxia commented 5 years ago

This looks great, thanks!

Sorry for the delay!