[Agda] operator treating

Andrew Morris lists at andy-morris.xyz
Sat Nov 7 21:45:37 CET 2015


> (fr′ n d d≢0) *fr (foo′ n' d' d'≢0) =  fr′ (n * n') (d * d') dd'≢0

There doesn't seem to be a foo' constructor declared anywhere; is it a typo for fr'?


More information about the Agda mailing list