Open JasonGross opened 10 years ago
Inductive test : $(let U := type of Type in exact U)$ := t. (* Anomaly: Unable to handle arbitrary u+k <= v constraints. Please report. *)