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
Sorry, can you provide a complete Agda file for reproduction?
I tried to reproduce this issue with the following file:
moduleIssue201wheredataN:SetwhereS : N -> N
Z : N
dataVec (A :Set) : N ->Setwhere[] : Vec A Z
_::::::::::::::::::::::::::::::::::::::::::::::::::::::::::_ : {n : N} -> A -> Vec A n -> Vec A (S n)
example : Vec N (S (S (S (S (S (S (S (S (S Z)))))))))
example ={! !}
I'd expect C-c C-a on the hole for example to give me a multiline result, and it did, with expected result:
example : Vec N (S (S (S (S (S (S (S (S (S Z)))))))))
example = Z ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
(Z ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
(Z ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
(Z ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
(Z ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
(Z ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
(Z ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
(Z ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
(Z ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
[]))))))))
The example above was generated with Agda-2.6.4, tried to ask Agda-2.7.0 to generate a solution but the new solver cannot find a solution somehow :|
When a multiline thing is generated using
C-c C-a
, newlines are printed instead of used as newlines:The text was updated successfully, but these errors were encountered: