dest_select
boolSyntax.dest_select : term -> term * term
Breaks apart a choice term into selected variable and body.
If M has the form @v. t then dest_select M returns (v,t).
Failure
Fails if M is not an epsilon-term.
Press ← or → to navigate between chapters
Press S or / to search in the book
Press ? to show this help
Press Esc to hide this help
dest_selectboolSyntax.dest_select : term -> term * term
Breaks apart a choice term into selected variable and body.
If M has the form @v. t then dest_select M returns (v,t).
Fails if M is not an epsilon-term.