ガリグ先生の講義の9番目の資料(ssrcoq9.v)で出てくる bigop について、mathcomp.ssreflect.bigop の冒頭を訳しました*1。ssrcoq9.v の中では Notation であるはずの \big[op/idx]_~ が Definition になっていたりして混乱しますが、直接定義だけを追うより全体像(=この文書の内容)を把握した方が早かったようです。 (といっても Tips の内容は全然分かってませんが…) 概要 This file provides a generic definition for iterating an operator over a…