Modules can contain `Implicit` types and values

antitypical / Manifold

An implementation of a dependently-typed intermediate language used by Tesseract.

MIT License

30 stars 0 forks source link

Modules can contain `Implicit` types and values #185

Open robrix opened 8 years ago

robrix commented 8 years ago

We might want to disallow implicit types (modulo #163). We should almost certainly disallow implicit values since it’s doubtful that unification suffices to infer unique inhabitants (and it’s essentially never useful to).