Menu
I would like to automatically case over arguments using a syntax declared besides the one given as a type constructor. For example,
postulate P : ℕ → ℕ → Set
data Silly : Set where
goo : (n : ℕ) → Fin n → (m : ℕ) → Fin m → P n m → Silly
Here, I'd like to have the proof P n m occur between the n and m arguments, but that cannot be since both need to be declare for it to be expressed. Hence, we use a syntax declaration:
syntax goo n i m j pf = i ⟵[ n , pf , m ]⟶ j
Now, we can write-up by-hand
want-to-use-syntax-in-pattern-matching : Silly → Set
want-to-use-syntax-in-pattern-matching (i ⟵[ n , pf , m ]⟶ j) = ℕ
This works fine, but when I case-split via C-c C-c, it uses goo instead of my syntax. Is there any way to make case splitting use my declared syntax ?
( Incidentally, using
syntax goo n i m j pf = i ─[ n , pf , m ]⟶ j
fails, where ─ is produced by \---
)
352
You can perform split by defining a value to the maxsplit parameter. If you put whitespaces as separator and the maxsplit value to be 2, the Split function splits the string into a list with maximum two items. Here, you can see the variable str is declared with a string of different subject names.
A split acts as a partition of a dataset: it separates the cases in a dataset into two or more new datasets.
Subsetting a SAS data set means extracting a part of the data set by selecting a fewer number of variables or fewer number of observations or both. While subsetting of variables is done by using KEEP and DROP statement, the sub setting of observations is done using DELETE statement.
Nowadays Agda resugars patterns on the left if they are in scope unqualified so this would just work.
138
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
