Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 15 Jun 2011 11:06:31 +0900] rev 2854
one TODO and one Problem?
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 15 Jun 2011 09:51:26 +0900] rev 2853
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 15 Jun 2011 09:50:53 +0900] rev 2852
Some TODOs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 15 Jun 2011 09:31:59 +0900] rev 2851
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 15 Jun 2011 09:25:36 +0900] rev 2850
TypeSchemes work with 'default'.
Christian Urban <urbanc@in.tum.de> [Tue, 14 Jun 2011 19:11:44 +0100] rev 2849
tuned some proofs
Christian Urban <urbanc@in.tum.de> [Tue, 14 Jun 2011 14:07:07 +0100] rev 2848
fixed the problem when giving a complex default-term; the fundef lemmas in Nominal_Base were not general enough
Christian Urban <urbanc@in.tum.de> [Tue, 14 Jun 2011 11:43:06 +0100] rev 2847
tuned
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 10 Jun 2011 15:52:17 +0900] rev 2846
Move working examples before non-working ones
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 10 Jun 2011 15:45:49 +0900] rev 2845
Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 10 Jun 2011 15:31:14 +0900] rev 2844
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 10 Jun 2011 15:30:09 +0900] rev 2843
Slightly modify fcb for list1 and put in common place.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 10 Jun 2011 09:00:24 +0900] rev 2842
Experiments with Let
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 09 Jun 2011 15:34:51 +0900] rev 2841
Eval can be defined with additional freshness
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 09 Jun 2011 15:03:58 +0900] rev 2840
Minor simplification
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 09 Jun 2011 11:10:41 +0900] rev 2839
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 09 Jun 2011 09:44:51 +0900] rev 2838
More experiments with 'default'
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 08 Jun 2011 21:44:03 +0900] rev 2837
Finished the proof with the invariant
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 08 Jun 2011 21:32:35 +0900] rev 2836
Issue with 'default'
Christian Urban <urbanc@in.tum.de> [Wed, 08 Jun 2011 12:30:56 +0100] rev 2835
merged
Christian Urban <urbanc@in.tum.de> [Wed, 08 Jun 2011 12:30:46 +0100] rev 2834
merged
Christian Urban <urbanc@in.tum.de> [Wed, 08 Jun 2011 08:44:01 +0100] rev 2833
using the option "default" the function package allows one to give an explicit default value
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 08 Jun 2011 17:52:06 +0900] rev 2832
Simpler proof of TypeSchemes/substs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 08 Jun 2011 17:25:54 +0900] rev 2831
Simplify fcb_res
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 08 Jun 2011 09:56:39 +0900] rev 2830
FCB for res binding and simplified proof of subst for type schemes
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 08 Jun 2011 07:06:20 +0900] rev 2829
Simplify ln-trans proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 08 Jun 2011 07:02:52 +0900] rev 2828
cbvs can be easily defined without an invariant
Christian Urban <urbanc@in.tum.de> [Tue, 07 Jun 2011 20:58:00 +0100] rev 2827
defined the "count-bound-variables-occurences" function which has an accumulator like trans
Christian Urban <urbanc@in.tum.de> [Tue, 07 Jun 2011 17:45:38 +0100] rev 2826
merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 07 Jun 2011 23:42:12 +0900] rev 2825
remove garbage (proofs that assumes the invariant outside function)