Skip to content

Commit d86c0ae

Browse files
committed
Add selftest for HOL-Theorem-Prover#1496
1 parent 8604837 commit d86c0ae

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

src/q/selftest.sml

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -435,6 +435,11 @@ val _ = require (check_result (fn _ => true))
435435
REWRITE_TAC [])
436436
([], ``p /\ T = p``)
437437

438+
val _ = tprint "PAT_ABBREV_TAC handles underscores"
439+
val _ = require (check_result (fn _ => true))
440+
(Q.PAT_ABBREV_TAC `bar = foo _`)
441+
([], ``_ y = foo a``)
442+
438443
val _ = new_definition ("gh425a_def", ``gh425a a = a``);
439444
val _ = new_definition ("gh425b_def", ``gh425b p = (p ==> T)``);
440445
val _ = overload_on ("gh425", ``gh425a``);

0 commit comments

Comments
 (0)