LIST_CONV : conv -> conv

SYNOPSIS

Apply a conversion to each element of a list.

DESCRIPTION

If cnv `ti` returns |- ti = ti' for i ranging from 1 to n, then LIST_CONV cnv `[t1; ...; tn]` returns |- [t1; ...; tn] = [t1'; ...; tn'].

FAILURE CONDITIONS

Fails if the conversion fails on any list element.

EXAMPLE

  # LIST_CONV num_CONV `[1;2;3;4;5]`;;
  val it : thm = |- [1; 2; 3; 4; 5] = [SUC 0; SUC 1; SUC 2; SUC 3; SUC 4]

USES

Applying a conversion more delicately than simply by DEPTH_CONV etc.