Tiger Abstract Syntax Format

TigerAbstractSyntaxFormat^? (Tiger-Abstract-Syntax-Format) is a format checker for Tiger abstract terms. It traverses a given term to see if it conforms to the desugared Tiger format, i.e., the term should be correct with respect to the Tiger signature and in addition only contain desugared expressions. The format checker is defined by means of the idiom of RecursivePattern.