agda-editor-tactics

Homepage: https://github.com/alhassy/next-700-module-systems

Author: Musa Al-hassy

Updated:

Summary

An editor tactic to produce Σ-types from Agda records

Commentary

Agda uses a number of editor tactics, such as C-c C-c, to perform case
analysis or to extract inner definitions to the toplevel.  We add a new
tactic.

Select an Agda record, then press M-x agda-editor-tactics-as-Σ:nested,
tabbing along the way, to obtain a transformed Σ-product form of the record.

This tactic was requested in the Agda mailing list,
I will likely produce other tactics as requested ---time permitting.

This file has been tangled from a literate, org-mode, file.

Dependencies