HRS Format
This format deals with higherorder rewrite systems (HRSs) described in
 R. Mayr and T. Nipkow. Higherorder rewrite systems and their confluence. Theoretical Computer Science, 192(1):3–29, 1998.
Format
The grammar of the format is given as follows.
spec ::= ( decl ) spec  e decl ::= VAR idlist  RULES rulelist  FUN idlist  id anylist anylist ::= e  any anylist any ::= id  \  ,  .  :  string  ( anylist ) sig ::= e  id : type sig rulelist ::= e  rule  rule , rulelist rule ::= term > term term ::= id  term ( termlist )  term term  \ idlist . term  ( term ) termlist ::= term  term , termlist idlist ::= id  id idlist type ::= type > type  id  ( type )Here id denotes nonempty sequences of characters except white space, '(', ')', '"', ',', '\', ':' and '.' and excluding the character sequences '>', 'FUN', 'RULES' and 'VAR'. The empty string is denoted by e and string denotes sequences of any characters.
Additionally the following constraints are imposed:
 At least one VAR, one FUN and one RULES declaration are mandatory. If there are several, the union is taken.
 An identifier declared in a VAR declaration must not be declared in a FUN declaration and vice versa.
 All identifiers occurring in rules must be declared (including bound variables).
 In types > associates to the right.
 Application associates to the left.
 Abstraction associates to the right.
 Abstractions extend as far to the right as possible (application binds stronger than abstraction).
 Term expression t (u_1,...,u_n) is syntactic sugar for (... (t u_1) ...) u_n note that due to leftassociativity of application s t(u,v) = (s t)(u,v) = (((s t) u) v).
 Term expression \ x_1 ... x_n . s is syntactic sugar for \ x_1 . ... \ x_n . s.

Terms must be typable according to the following rules:
x : T in VAR c : T in FUN s : T > S t : T x : T s : S     x : T c : T s t : S \x.s : T > S
The left and righthand side of a rewrite rule must be of the same base type.
Example
Examples of the format are given below:
(FUN abs : (term > term) > term app : term > term > term ) (VAR x : term S : term F : term > term ) (RULES app(abs(\x.F x),S) > F(S), abs(\x.app(S,x)) > S ) (COMMENT untyped lambda calculus with beta and eta)
(FUN 0 : nat s : nat > nat nil : natlist cons : nat > natlist > natlist map : (nat > nat) > natlist > natlist ) (VAR n : nat f : nat > nat h : nat t : natlist ) (RULES map (\n.f n) nil > nil, map (\n.f n) (cons h t) > cons (f h) (map (\n.f n) t) ) (COMMENT map on lists of natural numbers)