Built with
Alectryon. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl.
Require Import HoTT.Basics Fin.Require Import HoTT.Basics Fin.
(** ** Tactics *)
Ltac FinIndOn X := repeat
match type of X with
| Fin 0 => destruct X
| Empty => destruct X
| Unit => destruct X
| Fin ?n => destruct X as [X|X]
| ?L + Unit => destruct X as [X|X]
end.
(** This tactic can be used to generate n cases from a goal like forall (x : Fin n), _ *)
Ltac FinInd := let X := fresh "X" in intro X; FinIndOn X.