[Agda] Newbie question, book exercise problem.

[Nils Anders Danielsson]

On 2009-12-02 15:03, Paul Graphov wrote:
> When I remove the whole cong expression and replace it with {! !} ant then
> try to
> reduce tabulate(_!_ (x ∷ xs)) to normal form (C-c C-n) it gives "x ∷
> tabulate ((λ {.x} → _!_ (x ∷ xs)) ∘ fsuc)"

For me it gives "x ∷ tabulate (_!_ xs)".

--
/NAD