> Maybe I've misunderstood this as a misunderstanding. The example term
> representation for the YXML library is exactly the Isabelle term datatype.
> But that is really just an example, it is not really useful for the
> problem to connect users to proof checkers.
Oh, I see.
No, it does seem to be the case that Coq's term is much more complicated
than Isabelles. The analogous datatype for proofterm would be something
like:
type env = {
env_globals : globals;
env_named_context : named_context;
env_named_vals : named_vals;
env_rel_context : rel_context;
env_rel_val : lazy_val list;
env_nb_rel : int;
env_stratification : stratification;
retroknowledge : Retroknowledge.retroknowledge }
for the environment.
Edward
_______________________________________________
ProofGeneral-devel mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
