summaryrefslogtreecommitdiff
path: root/test-suite/output/Cases.v
blob: 452d3603628711f24f1cdf41840e92a1c642747c (plain)
1
2
3
4
5
6
(* Cases with let-in in constructors types *)

Inductive t : Set :=
    k : let x := t in x -> x.

Print t_rect.