namedCases_on

BasicProvers.namedCases_on : term quotation -> string list -> tactic

Case split on type of supplied term, using given names for introduced constructor arguments.

bossLib.namedCases_on is identical to BasicProvers.namedCases_on.

See also

bossLib.namedCases, bossLib.Cases_on, bossLib.Cases