#
e13bfb29 |
|
26-Oct-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Move lambda type, dest_term function to kernel; add identical fn dest_term is quite heavily used (it implements SML's best approximation of a "view" for pattern-matching against terms), and its implementation outside the kernel is needlessly inefficient. Also extend signature with identical function, which correctly says whether or not two terms are identical, including in their choice of bound names. In the standard kernel, the possible presence of explicit substitution terms means that this notion is not the same as simple equality on terms.
|