"git-rts@gitlab.mpi-sws.org:adamAndMath/stdpp.git" did not exist on "1a98fc894dedd65d98c7b1f447899de594937d46"
Fix documentation of `select` to state that it selects the "last" hypothesis.
1 unresolved thread
1 unresolved thread
Merge request reports
Activity
mentioned in merge request iris!625 (merged)
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 changed this line in version 3 of the diff
added 1 commit
- d0d98a8e - Fix documentation of `select` to state that it selects the "last" hypothesis.
mentioned in commit e97b9309
Please register or sign in to reply