This releases adds higher-order logic functionality to Athena, enabling quantification over functions.
-
Sorts of the form (Fun S_1 ... S_n T) now accepted
-
Arbitrary app terms accepted now
-
Auto-adding lifted symbol versions
-
Handled unary app cases
-
Restored infix_parser.sml
-
Overloaded and input-expanded symbols now also do term lifting as needed
-
uspec now accepts higher-order values as the second argument
-
Explicit app's of lifted symbols are now auto-simplifed in AT.makeApp1 rather than the evaluator level
-
Added primitive method functor-identity
-
Examples in sf/code/hol4.ath working
-
Proper 'app' sort checking for unary, binary, and general applications
-
Checking in lib/basic/hol_examples.ath
-
Implemented promotion of anonymous lambdas