<div dir="ltr">I&#39;ve enjoyed playing with the 2.5.1 RC so far.  The new library management seems very nice, sections have proven to be immediately valuable, and I&#39;m looking forward to playing with the new reflection and other features.<div><br></div><div>I&#39;ve been going through Software Foundations and doing the exercises in Agda in a &quot;pure functional&quot; style with no tactics (not even Agda&#39;s rewrite); so far I far prefer the results I&#39;ve been able to obtain to Coq&#39;s tactics--I feel the functional style is simpler and clearer.  This may change as the proofs get more complicated.  I&#39;m about midway through the &quot;More Coq&quot; chapter now and so far I only miss the unfold and inversion tactics, but I&#39;ve been able to work around them with a little effort.</div><div><br></div><div>I have noticed one &quot;regression&quot; of sorts regarding sym of propositional equality--when goals are shown with C-c C-, sym is represented as &quot;Function.flip&quot; whereas before the flip was done explicitly.  As a simple example, in the following (I&#39;ve written it to show two calls to sym):</div><div><br></div><div><div><font face="monospace, monospace">n+0=n : (n : ℕ) → n + 0 ≡ n</font></div><div><font face="monospace, monospace">n+0=n zero    = refl</font></div><div><font face="monospace, monospace">n+0=n (suc n) = cong suc (n+0=n (n))</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">m+Sn : (m n : ℕ) → m + suc n ≡ suc (m + n)</font></div><div><font face="monospace, monospace">m+Sn zero    n = refl</font></div><div><font face="monospace, monospace">m+Sn (suc m) n = cong suc (m+Sn m n)</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">+comm : (m n : ℕ) → m + n ≡ n + m</font></div><div><font face="monospace, monospace">+comm zero    n =</font></div><div><font face="monospace, monospace">  let a = sym (n+0=n n)</font></div><div><font face="monospace, monospace">  in {!!}</font></div><div><font face="monospace, monospace">+comm (suc m) n =</font></div><div><font face="monospace, monospace">  let a = cong suc (+comm m n) </font></div><div><font face="monospace, monospace">      b = sym (m+Sn n m)</font></div><div><font face="monospace, monospace">  in {!!}</font></div></div><div><br></div><div>In the first hole we get</div><div><br></div><div><div><font face="monospace, monospace">Goal: n ≡ n + zero</font></div><div><font face="monospace, monospace">————————————————————————————————————————————————————————————</font></div><div><font face="monospace, monospace">a : Function.flip _≡_ (n + 0) n</font></div><div><font face="monospace, monospace">n : ℕ</font></div></div><div><br></div><div>and in the second hole </div><div><br></div><div><div><font face="monospace, monospace">Goal: suc (m + n) ≡ n + suc m</font></div><div><font face="monospace, monospace">————————————————————————————————————————————————————————————</font></div><div><font face="monospace, monospace">b : Function.flip _≡_ (n + suc m) (suc (n + m))</font></div><div><font face="monospace, monospace">a : suc (m + n) ≡ suc (n + m)</font></div><div><font face="monospace, monospace">n : ℕ</font></div><div><font face="monospace, monospace">m : ℕ</font></div></div><div><font face="monospace, monospace"><br></font></div><div><font face="arial, helvetica, sans-serif">In the previous version these would have been </font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="monospace, monospace">a : n ≡ (n + 0)</font></div><div><span style="font-family:monospace,monospace"><br></span></div><div><font face="arial, helvetica, sans-serif">and</font></div><div><span style="font-family:monospace,monospace"><br></span></div><div><span style="font-family:monospace,monospace">b : </span><span style="font-family:monospace,monospace">suc (n + m)</span><span style="font-family:monospace,monospace"> ≡ (n + suc m) </span></div><div><span style="font-family:monospace,monospace"><br></span></div><div><font face="arial, helvetica, sans-serif">respectively, which are certainly easier to read.</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">I can still read the Function.flip notation but it was easier to read in the previous version, so if this is viewed as a regression I&#39;m happy to file an issue for it.</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">John</font></div><div><span style="font-family:monospace,monospace"><br></span></div></div>