lemma-overloading icon indicating copy to clipboard operation
lemma-overloading copied to clipboard

Published 20 hours ago • verified publisher icon coq-community

Fix

Open pi8027 opened this issue 8 months ago • 1 comments

Currently, Lemma Overloading does not compile with Rocq 9.0, MathComp 2.3, and HB 1.8.1.

Error:
HB: choice.hasChoice.axioms_ is not a factory or its library (mathcomp.ssreflect.choice) was not correctly imported

pi8027 avatar Mar 28 '25 20:03 pi8027