Size: a a a
I
I
class InnerState {
is SomeMsg -> this.onSomeMsg(true)
}class OuterState(s: InnerState) {
is SomeMsg -> s.onSomeMsg(false)
}onSomeMsg может вернуть не только новый стейт, который просто заново обернешь в OuterState, но еще и команды :(ML
((Unit) -> T).invoke() = invoke(Unit)(
((Unit) -> T).invoke() = invoke(Unit)I
Sλ
AD
AD
QH
((Unit) -> T).invoke() = invoke(Unit)ML
O
QH
MM
(
data State : Type where
MkState : (ct : Nat) -> (tabs : Vect (ct + m) a) -> State
state : State
state = MkState 2 (MkTab :: Nil)
|
13 | a = MkState 2 (MkTab :: Nil)
| ~~
When checking right hand side of a with expected type
State
When checking an application of constructor Playground.:::
Type mismatch between
Vect 0 a (Type of [])
and
Vect (S m) Tab (Expected type)
Specifically:
Type mismatch between
0
and
S m
I
data State : Type where
MkState : (ct : Nat) -> (tabs : Vect (ct + m) a) -> State
state : State
state = MkState 2 (MkTab :: Nil)
|
13 | a = MkState 2 (MkTab :: Nil)
| ~~
When checking right hand side of a with expected type
State
When checking an application of constructor Playground.:::
Type mismatch between
Vect 0 a (Type of [])
and
Vect (S m) Tab (Expected type)
Specifically:
Type mismatch between
0
and
S m
(
AM
AM
I
> пойду к реакту идрис прикручивать
(