Skip to content
Snippets Groups Projects

Fix documentation of `select` to state that it selects the "last" hypothesis.

Merged Robbert Krebbers requested to merge robbert/select_last into master
1 unresolved thread

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
508 508 Ltac unblock_goal := unfold block in *.
509 509
510 510
511 (** [select] finds the first hypothesis matching [pat] and passes it
512 to the continuation [tac]. Its main advantage over using [match goal
513 with ] directly is that it is shorter. If [pat] matches multiple
514 hypotheses, then [tac] will only be called on the first matching
515 hypothesis. If [tac] fails, [select] will not backtrack on subsequent
516 matching hypotheses.
517
518 [select] is written in CPS and does not return the name of the
511 (** The tactic [select pat tac] finds the first hypothesis matching [pat] and
512 passes it to the continuation [tac]. Its main advantage over using [match goal
513 with ] directly is that it is shorter. If [pat] matches multiple hypotheses,
514 then [tac] will only be called on the last (i.e., bottommost) matching
  • added 1 commit

    • d0d98a8e - Fix documentation of `select` to state that it selects the "last" hypothesis.

    Compare with previous version

  • Robbert Krebbers added 2 commits

    added 2 commits

    • 06531b45 - Fix documentation of `select` to state that it selects the "last" hypothesis.
    • cf9f43cb - Expand comment in `select`; based on `iSelect` in Iris.

    Compare with previous version

  • I also updated the comment in this tactic based on the more detailed comment for iSelect in Iris.

  • Ralf Jung resolved all threads

    resolved all threads

  • merged

  • Ralf Jung mentioned in commit e97b9309

    mentioned in commit e97b9309

  • Please register or sign in to reply
    Loading