Fix lexp's Induction to name fields. Fix lexp_context for real vars.
* src/debruijn.ml (db_idx, db_ridx): Re-introduce those type aliases. (senv_add_var): Remove redundancy. Change calling convention. (lexp_context): Make var's "value" optional. (env_extend): New function. * src/eval.ml (nfirst_rte_var._eval.ctor_name): Fix confusion in constructor args. * src/lexp.ml (lexp): Add optional name to constructor fields. * src/lparse.ml (default_lctx): Adjust to new senv_add_var. (lexp_parse): Consolidate the two Plambda cases. Don't mess with local_scope here. (lexp_parse_inductive): Rename from lexp_parse_constructors. Adapt to lexp changes. Use List.fold_left. (lexp_decls): Adjust to new senv_add_var. (lexp_context_print): Handle vars without value.
Loading
Please register or sign in to comment