| 123456789101112131415161718192021222324252627282930313233 |
- Thoughts on mutual declarations
- -------------------------------
- When checking block of mutual declarations
- x1 : A1
- x1 = e1
- ...
- xn : An
- xn = en
- you first check that (x1:A1)..(xn:An) is a well-formed context and then you
- check that e1..en fits this context. Basically we decouple the types from the
- definitions.
- How can we extend this to datatypes and definitions by pattern matching? What
- would the ei's be? An attempt:
- data Declaration = ... | Definition Telescope [Definition]
- data Definition = FunDef DefInfo Name [Clause]
- | DataDef DefInfo [LamBinding] [Constructor]
- -- ^ domain-free bindings matching the telescope
- I don't see a problem with this approach. Let's try it and see how far we get...
- Untyped definitions doesn't fit this.. but they shouldn't appear in a mutual
- anyway so let's make a special case for those:
- data Declaration = ... | UntypedDefinition DefInfo Name Expr [Declaration]
|
