Then I get an obscure error message telling me there's a type mismatch. No there's not. A parameter should shadow whatever Prelude brings in
-
-
Replying to @anormalform
While I'm at it: I'd like to use vars starting with a Capital without it guessing it's a Cons. I want to write `(a : A)`, not `(eltA : a)`.
1 reply 0 retweets 1 like -
-
Replying to @anormalform
@eisaru There are rules for this… it isn't trying to read your mind.
2 replies 0 retweets 0 likes -
Replying to @edwinbrady
@eisaru Even so, can you show me your code? Error messages should explain this problem, and ought to have got better recently.
2 replies 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady After minimisation: this is broken http://lpaste.net/158422 and this works http://lpaste.net/1584231 reply 0 retweets 0 likes -
Replying to @anormalform
@eisaru That's certainly consistent with the rules…
2 replies 0 retweets 0 likes -
Replying to @edwinbrady
@eisaru …though thinking about it, perhaps as lt is a parameter, the rules are wrong here. Some more thought needed, perhaps.
1 reply 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady PE Dagand had a fairly nice syntax to allow the sort of interleaving of parameters & indices you have whilst still tagging them.1 reply 0 retweets 0 likes -
Replying to @anormalform
@edwinbrady IIRC, params were between "[...]" whilst indices were between "(...)". So you'd have `data Vect : [a : Set] -> (n : Nat) -> Set`1 reply 0 retweets 0 likes
@eisaru Hmm, I wouldn't mind a way to make parameters explicit. But I'm not sure I like that one though due to list syntax. Will think more.
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.