infotheo icon indicating copy to clipboard operation
infotheo copied to clipboard
verified publisher icon affeldt-aist

fix coercions from prob to algebraic structures

Open t6s opened this issue 2 months ago • 1 comments

This PR fixes some coercions so that, for example,

Variables (R : realType) (x y : R).
Check x + y.

succeeds.

t6s avatar Nov 06 '25 15:11 t6s

turned into a draft until I figure out how to handle mc master

t6s avatar Nov 06 '25 17:11 t6s