Skip to content

pool optim, toward only head normal term added to the pool #26

@craff

Description

@craff

insert_t_node should use a stack to avoid creating node for partially applied function.

For instance, adding [add n p] to the pool also adds [add n] which is a lambda, hence trigger a cloture construction.

This cost is dominating "equiv" when computation are really needed, with
probably a factor much greater that 2 (10 ?) to gain.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions