basic_convs : unit -> (string * (term * conv)) list

SYNOPSIS

List the current default conversions used in rewriting and simplification.

DESCRIPTION

The HOL Light rewriter (REWRITE_TAC etc.) and simplifier (SIMP_TAC etc.) have default sets of (conditional) equations and other conversions that are applied by default, except in the PURE_ variants. A call to basic_convs() returns the current set of conversions.

FAILURE CONDITIONS

Never fails.

EXAMPLE

In the default HOL Light state the only conversions are for generalized beta reduction and the reduction of pattern-matching constructs such as match...with. All the other default simplifications are done by rewrite rules.

  # basic_convs();;
  val it : (string * (term * conv)) list =
    [("FUN_ONEPATTERN_CONV", (`_FUNCTION (\y z. P y z) x`, ));
     ("MATCH_ONEPATTERN_CONV", (`_MATCH x (\y z. P y z)`, ));
     ("FUN_SEQPATTERN_CONV", (`_FUNCTION (_SEQPATTERN r s) x`, ));
     ("MATCH_SEQPATTERN_CONV", (`_MATCH x (_SEQPATTERN r s)`, ));
     ("GEN_BETA_CONV", (`GABS (\a. b) c`, ))]