On 2 April 2015 at 14:57, Matt Oliveri <[email protected]> wrote: > On Thu, Apr 2, 2015 at 9:50 AM, Keean Schupke <[email protected]> wrote: > > On 2 April 2015 at 14:25, Matt Oliveri <[email protected]> wrote: > >> You seem to be under the hilarious misimpression that everything in > >> MLTT is a type. It ain't so! Ask any proof assistant: "fun (x : 4) => > >> x" is nonsense. > > > > There is nothing fundamentally wrong with that statement, I could write; > > > > fun (x : succ (succ (succ (succ zero)))) => x > > > > So I could allow "4" so be a shorthand for succ (succ (succ (succ zero))) > > and then hide the succ/zero types inside a module. > > No no no. 4 _is_ a shorthand for that. (Modulo constructor names.) > (succ (succ (succ (succ zero)))) isn't a type.
Now, that seems unexpected. Why is it not a type? Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
