Files
emacs/snippets/coq-mode/tactics/induction.yasnippet
2024-04-30 07:08:23 +02:00

6 lines
114 B
Plaintext

# -*- mode: snippet -*-
# key: ind
# group: tactics
# name: induction
# --
induction ${1:n} as [ | $1' IH_$1' ].$0