On 2012-05-04 17:09, Wolfgang Jeltsch wrote: > I propose to use an alternative syntax, maybe the following: > > syntax Σ A (λ x → B) = Σ[ x ∈ A ] B I switched to this syntax. I also renamed Function.type-signature to _∋_, and removed the "x ∶ A" syntax for it. -- /NAD