You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
If we define a type inside a namespace and it's not publicly exported, then we shouldn't be able to pattern match over its definition. This works fine, as the interactive editing tools don't offer the option to case split in that scenario.
The problem arises when trying to case split while being inside the same namespace (which should be possible, but it's not offered by the interactive tools).
Steps to Reproduce
Consider the following code:
import Data.Vect
namespace StackStack:Nat->TypeStack n =Vect n Stringpop: Stack (S n) -> (String, Stack n)
pop stack =?pop_rhs
-- ^^^^^ trying to case split here
Expected Behavior
Case splitting should be possible, leaving the pop function like this:
pop: Stack (S n) -> (String, Stack n)
pop (x :: xs) =?pop_rhs_0
-- ^^^^^^^^^
Observed Behavior
If we try to case split the stack parameter, no option is offered:
Additional notes
Case splitting does work fine if we publicly export the definition of Stack:
import Data.Vect
namespace Stack
public export
Stack:Nat->TypeStack n =Vect n Stringpop: Stack (S n) -> (String, Stack n)
pop stack =?pop_rhs
-- ^^^^^ trying to case split here works fine
Or when we're not working inside of a namespace:
import Data.Vect
Stack:Nat->TypeStack n =Vect n Stringpop: Stack (S n) -> (String, Stack n)
pop stack =?pop_rhs
-- ^^^^^ trying to case split here works fine
It also works fine by not allowing to case split if we're outside of the namespace and the definition was not publicly exported:
import Data.Vect
namespace Stack
export
Stack:Nat->TypeStack n =Vect n Stringpop: Stack (S n) -> (String, Stack n)
pop stack =?pop_rhs_0
-- ^^^^^ trying to case split here does nothing, which is correct
The text was updated successfully, but these errors were encountered:
Problem
If we define a type inside a namespace and it's not publicly exported, then we shouldn't be able to pattern match over its definition. This works fine, as the interactive editing tools don't offer the option to case split in that scenario.
The problem arises when trying to case split while being inside the same namespace (which should be possible, but it's not offered by the interactive tools).
Steps to Reproduce
Consider the following code:
Expected Behavior
Case splitting should be possible, leaving the
popfunction like this:Observed Behavior
If we try to case split the
stackparameter, no option is offered:Additional notes
Case splitting does work fine if we publicly export the definition of
Stack:Or when we're not working inside of a namespace:
It also works fine by not allowing to case split if we're outside of the namespace and the definition was not publicly exported:
The text was updated successfully, but these errors were encountered: