No index entry for `model_check` tactic
Closed this issue · 1 comments
bkushigian commented
I'm not seeing an index entry for the model_check
tactic. This is conceptually a simple enough tactic that it probably doesn't matter, but mentioning it in case this was an oversight.
achlipala commented
Yeah, that connects to an interesting didactic question. The tactics documented in that index are meant to be used throughout the book, whereas recommended use of model_check
is concentrated narrowly -- it's really meant mostly as a supplement to certain chapters. I also think it would need significantly more documentation than the other tactics, depending more on definitions from the book library, etc., so I think I'll hold off on adding an entry for now.