[Agda] Type a = Set a
Andreas Abel
abela at chalmers.se
Sun May 31 10:01:28 CEST 2015
I do not expect any problems. Agda will still talk about `Set' in error
messages, though...
On 30.05.2015 21:06, Sergei Meshveliani wrote:
> People,
> I consider renaming `Set' to `Type' this way:
>
> Type : (a : Level) → Set (suc a)
> Type a = Set a
>
> The idea is to write `Type' everywhere instead of `Set'.
> Will this work all right?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list