search

Orbis-Tertius / osl

Apache License 2.0
2 stars 2 forks source link

Allow arguments inline in declarations #21

Open morganthomas opened 2 years ago

morganthomas commented 2 years ago

Example:

foo (x : N) : N -> Prop
  := \y : N => x = y.

Instead of:

foo : N -> N -> Prop
  := \x : N => \y : N => x = y.