chrisamaphone, 1 month ago i guess the question i'm asking is, if this is proof general, then why doesn't agda (/lean/everything other than uh rocq and isabelle?) use it? i'm not asking rhetorically; i'd like to have a better understanding of its shortcomings
i guess the question i'm asking is, if this is proof general, then why doesn't agda (/lean/everything other than uh rocq and isabelle?) use it?
i'm not asking rhetorically; i'd like to have a better understanding of its shortcomings