Skip to content

Revise the axiom for definedness #439

@berpeti

Description

@berpeti

Instead of using $\lceil x \rceil \in \Gamma$ for some concrete $x$ in the definedness axiom, we should use for all evars $x$, we have $\lceil x \rceil \in \Gamma$. This way, we can use the definedness axiom for any variable, which is necessary if we have to make sure that this variable is fresh in some pattern (e.g., for the side condition of the deduction theorem).

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions