Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-08 20:57:14 -0800 (Tue, 08 Feb 2005)
Revision: 6638
Log message:
Collected the resource state into a record. Aleksey, can some of the
resource state can be pruned? I imagine the global_processed_data is
particularly large, and can be reconstructed if needed.
# abandon_all ();;
Mp_resource:
global_data = 330
local_data = 0
local_names = 0
top_data = 329
theory_include = 330
global_bookmarker = 3141
global_processed_data = 6265
() : unit
-------------------
A bit better info on type variables. Here is the error on
sequent { <H> >- 'C } --> sequent { <H> >- 'A }
type error:
- sequent [Syntax_test!sequent_arg] { <'H> >- 'C<|!|> }
- while typechecking
- 'C<|!|>
- context variable <H>
- has type
- Perv!ty_sequent_context_var
{Perv!ty_sequent_context_cvars{Perv!xnil};
Perv!ty_sequent_context_args{Perv!xnil};
Perv!ty_hyp{Perv!Term; Perv!Term}}
- but is used with type
- Perv!type[arg1022:v]
I've always been a bit confused about the notation 'C<|!|>. The
actual term here is 'C<|H|>, which might help clarify the error
message a bit.
Are these terms like 'x<|!|> the same as !x?
Why does 'C<|!|> print that way when it is actually 'C<|H|>?
Certainly we can do better, but I'd like to know why this doesn't
print as expected (Simple_print).