Cases.v « output « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

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

blob: 7483e8c40d1d6dd50b19d6d20452435126543502 (plain)

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

Inductive t : Set := k : [x:=t]x -> x.

Print t_rect.