freesin : term list -> term -> bool

SYNOPSIS

Tests if all free variables of a term appear in a list.

DESCRIPTION

The call freesin l t tests whether all free variables of t occur in the list l. The special case where l = [] will therefore test whether t is closed (i.e. contains no free variables).

FAILURE CONDITIONS

Never fails.

EXAMPLE

  # freesin [] `!x y. x + y >= 0`;;
  val it : bool = true
  # freesin [] `x + y >= 0`;;
  val it : bool = false
  # freesin [`x:num`; `y:num`; `z:num`] `x + y >= 0`;;
  val it : bool = true

USES

Can be attractive to fold together some free-variable tests without explicitly constructing the set of free variables in a term.

SEE ALSO

frees, freesl, vfree_in.