L11: decide graded necessity, spec QTT grade propagation — and fix Modal.idr, which had never compiled - #51

L11: decide graded necessity, spec QTT grade propagation — and fix Modal.idr, which had never compiled#51

hyperpolymath merged 1 commit into

mainhyperpolymath/ideas-to-alphas:mainfrom

feat/l11-qtt-integrationhyperpolymath/ideas-to-alphas:feat/l11-qtt-integrationCopy head branch name to clipboard