Skip to content

GitLab

Open
Created by Gergő Érdi@cactusContributor

Pattern synonym used in an expression context could have different constraints to pattern used in a pattern context

The two directions of an explicitly-bidirectional pattern might have utterly different class constraints. After all, the two directions are specified by quite different code. Suppose that

  • Pattern P (used in a pattern) requires constraints CR, and provides constraints CP
  • Constructor P (used in an expression) requires constraints CE

Then I think the only required relationship is this: CP must be provable from CE (since CP is packaged up in a P-object).

Currently, CE := CP + CR.

Edited by Matthew Pickering
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information