dest_term

Term.dest_term : term -> lambda

Breaks terms into a type with SML constructors for pattern-matching.

A call to dest_term t returns a value of type lambda, which has SML definition

   datatype lambda =
      VAR of string * hol_type
    | CONST of {Name:string, Thy:string, Ty:hol_type}
    | COMB of term * term
    | LAMB of term * term

This type encodes all possible forms of term.

Failure

Never fails.

Example

> dest_term ``SUC 2``;
val it =
   COMB
    (Const
      ({epoch = 0, name = {Name = "SUC", Thy = "num"}, uptodate = ref true},
       GRND
        (
           Tyapp
            (({epoch = 0, name = {Name = "fun", Thy = "min"}, uptodate =
               ref true}, 2),
             [Tyapp
               (({epoch = 0, name = {Name = "num", Thy = "num"}, uptodate =
                  ref true}, 0), []),
              Tyapp
               (({epoch = 0, name = {Name = "num", Thy = "num"}, uptodate =
                  ref true}, 0), [])])
           )),
     Comb
      (Const
        ({epoch = 0, name = {Name = "NUMERAL", Thy = "arithmetic"},
          uptodate = ref true},
         GRND
          (
             Tyapp
              (({epoch = 0, name = {Name = "fun", Thy = "min"}, uptodate =
                 ref true}, 2),
               [Tyapp
                 (({epoch = 0, name = {Name = "num", Thy = "num"}, uptodate =
                    ref true}, 0), []),
                Tyapp
                 (({epoch = 0, name = {Name = "num", Thy = "num"}, uptodate =
                    ref true}, 0), [])])
             )),
       Comb
        (Const
          ({epoch = 0, name = {Name = "BIT2", Thy = "arithmetic"}, uptodate =
            ref true},
           GRND
            (
               Tyapp
                (({epoch = 0, name = {Name = "fun", Thy = "min"}, uptodate =
                   ref true}, 2),
                 [Tyapp
                   (({epoch = 0, name = {Name = "num", Thy = "num"},
                      uptodate = ref true}, 0), []),
                  Tyapp
                   (({epoch = 0, name = {Name = "num", Thy = "num"},
                      uptodate = ref true}, 0), [])])
               )),
         Const
          ({epoch = 0, name = {Name = "ZERO", Thy = "arithmetic"}, uptodate =
            ref true},
           GRND
            (
               Tyapp
                (({epoch = 0, name = {Name = "num", Thy = "num"}, uptodate =
                   ref true}, 0), [])
               ))))): lambda

See also

Term.dest_abs, Term.dest_comb, Term.dest_const, boolSyntax.dest_strip_comb, Term.dest_thy_const, Term.dest_var