Equations
- psum.alt.sizeof (psum.inr b) = sizeof b
- psum.alt.sizeof (psum.inl a) = sizeof a
def
psum.has_sizeof_alt
(α : Type u)
(β : Type v)
[has_sizeof α]
[has_sizeof β] :
has_sizeof (psum α β)
Equations
- psum.has_sizeof_alt α β = {sizeof := psum.alt.sizeof _inst_2}
Argument for using_well_founded
The tactic rel_tac
has to synthesize an element of type (has_well_founded A).
The two arguments are: a local representing the function being defined by well
founded recursion, and a list of recursive equations.
The equations can be used to decide which well founded relation should be used.
The tactic dec_tac
has to synthesize decreasing proofs.