[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Handle 'lambda' and '@' in TIP theorems
- Subject: Re: Handle 'lambda' and '@' in TIP theorems
- From: Chris Warburton
- Date: Thu, 16 Nov 2017 12:26:17 +0000
- In-reply-to: <9ea9335503efe106-0-artemis@nixos>
- References: <9ea9335503efe106-0-artemis@nixos>
Added fix and regression tests for simplifying (@ f x) to just (f x) in
theorem statements.
This only applies to two theorems:
- tip2015/list_return_1.smt2
- tip2015/list_assoc.smt2
The latter also contains a lambda, so it's ruled out anyway.