concrete linsCnc of lins = { lincat Nat = {} ; -- we expect warnings because the lines bellow are commented out -- we don't expect warning for zero because Nat = {} -- lincat C = {s : Str} ; -- lin test = {s = "test"} ; }