You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Mutual induction schemes are not indented properly. Multiple with additions are indented like so:
Scheme a_mut := Induction for a Sort Prop
with b_mut := Induction for b Sort Prop
with c_mut := Induction for c Sort Prop
with d_mut := Induction for d Sort Prop.
It seems like this would have to follow the same pattern of indentation as mutually recursive fixpoints.
The text was updated successfully, but these errors were encountered:
Mutual induction schemes are not indented properly. Multiple
with
additions are indented like so:It seems like this would have to follow the same pattern of indentation as mutually recursive fixpoints.
The text was updated successfully, but these errors were encountered: