Agda のflag

なんか、

{-# OPTIONS --cubical-compatible --safe #-}

とすると、いろいろ出るエラーのうち

--warning=noUnsupportedIndexedMatch

を抑制していたみたい。それでいいっていいえばよいんだが、時間はあるので修正してます

他の部分も割と順調

学生のいない気楽さか