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. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
