Agda.TypeChecking.SyntacticEquality

Instantiate full as long as things are equal

Syntactic equality check for terms. If syntactic equality checking has fuel left, then checkSyntacticEquality behaves as if it were implemented in the following way (which does not match the given type signature), only that v and v' are only fully instantiated to the depth where they are equal (and the amount of fuel is reduced by one unit in the failure branch): checkSyntacticEquality v v' s f = do (v, v') <- instantiateFull (v, v') if v == v' then s v v' else f v v' If syntactic equality checking does not have fuel left, then checkSyntacticEquality instantiates the two terms and takes the failure branch.

Note that in either case the returned values v and v' cannot be MetaVs that are instantiated.

Syntactic equality check for terms without checking remaining fuel.

Does the syntactic equality check have any remaining fuel?