Currently, the proof output produces long normal form proofs (ie. beta-normal eta-long proofs). This makes sense from the point of view of proof search, but can be more user-friendly to produce eta-normal proofs as well.
Add an (optional) proof transformation step which transforms long normal form proofs into beta-eta-normal proofs.
Currently, the proof output produces long normal form proofs (ie. beta-normal eta-long proofs). This makes sense from the point of view of proof search, but can be more user-friendly to produce eta-normal proofs as well.
Add an (optional) proof transformation step which transforms long normal form proofs into beta-eta-normal proofs.