Cases.v « output « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/output/Cases.v

blob: 452d3603628711f24f1cdf41840e92a1c642747c (plain)

(* Cases with let-in in constructors types *)

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

Print t_rect.