[isabelle] Derive shows with List
when trying to derive a "show" class for a datatype, it fails with a
strange error if teh type has nested lists. Find attached a minimal
Am I doing something wrong here?
Thanks in advance for any help,
Isabelle2017 with AFP:
imports Main "Show.Show_Instances"
datatype 'a foo = C "'a list"
derive "show" foo
deriving "show" instance for type "Scratch.foo"
generating show-function for type "Scratch.foo"
1. (λxa. shows_pl p (shows_string ''C'' (shows_space (pshowsp_list 1
(map (show⇩'⇩a 1) x) (shows_pr p xa))))) =
(λxa. shows_pl p (shows_string ''C'' (shows_space (pshowsp_list 1
(map (show⇩'⇩a 0) x) (shows_pr p xa)))))
The error(s) above occurred for the goal statement⌂:
showsp_foo show⇩'⇩a p (C x) = shows_pl p ∘ shows_string ''C'' ∘
shows_space ∘ showsp_list show⇩'⇩a 1 x ∘ shows_pr p
This archive was generated by a fusion of
Pipermail (Mailman edition) and