Open UlfNorell opened 10 years ago
From andreas....@gmail.com on November 17, 2013 23:47:09
Sometimes you would like to have the record constructor in scope in the record module. For example, when defining O'Connor's Store comonad:
record Store (I O : Set) : Set where constructor store field peek : I → O pos : I
extract : O extract = peek pos
extend′ : ∀ {B} → (Store I O → B) → Store I B extend′ f = store (f ∘ store peek) pos
-- not in scope: store
A workaround is using copatterns:
extend′ : ∀ {B} → (Store I O → B) → Store I B pos (extend′ f) = pos peek (extend′ f) = f ∘ s where s : I → Store I O peek (s i) = peek pos (s i) = i
but it is a bit clumsy.
This report is part of the "record declarations might need some overhaul" series, see issue 966 for the start of a pointer chain.
Original issue: http://code.google.com/p/agda/issues/detail?id=967
From andreas....@gmail.com on November 17, 2013 23:47:09
Sometimes you would like to have the record constructor in scope in the record module. For example, when defining O'Connor's Store comonad:
record Store (I O : Set) : Set where constructor store field peek : I → O pos : I
extract : O extract = peek pos
extend′ : ∀ {B} → (Store I O → B) → Store I B extend′ f = store (f ∘ store peek) pos
-- not in scope: store
A workaround is using copatterns:
extend′ : ∀ {B} → (Store I O → B) → Store I B pos (extend′ f) = pos peek (extend′ f) = f ∘ s where s : I → Store I O peek (s i) = peek pos (s i) = i
but it is a bit clumsy.
This report is part of the "record declarations might need some overhaul" series, see issue 966 for the start of a pointer chain.
Original issue: http://code.google.com/p/agda/issues/detail?id=967