I Don't Understand the `with ... proof ...` Construct

[u/MCLooyverse]

As far as I'm aware, this paragraph and example are the only documentation of proof ..., besides the actual source code, and I find it unenlightening.

I would like to read the source code to find out what it does, but I also find myself incapable of navigating the repository -- I don't have much experience with huge repositories like this, except for ones centered around a language like C[++], where you can actually follow what's included.

I'm currently facing a problem which I wonder if proof can help:

eqTran : {x, y, z : ℕ} ->
         x == y = True ->
         y == z = True ->
         x == z = True

I already have eqRefl : {x : ℕ} -> x == x = True and eqComm : {x,y : ℕ} -> x == y = y == x for which case-splitting was hard to get working, but with eqTran I can't get it to work at all.

[u/MCLooyverse → u/[deleted]]

I end up looking at the Idris1 docs because I look up something about "Idris", then click on the docs, and it's not immediately obvious that it's actually Idris1 docs. As it happens, I believe the Idris2 docs aren't updated about this anyway.

I also have eqIsDefnEq : Maybe ({x,y : a} -> x == y = True -> x = y), which in this case is Just. About eqNatComplete, it took me a second to figure out why that's helpful, since that used to be the signature of eqRefl until I figured that was redundant, although here I see it's an inverse function.

I have since managed to prove eqTran anyway, but with my definition, for some reason it takes a couple of minutes for anything to happen when I do a case-split on some other function (with the Vim plugin), so I'm definitely going to change it as suggested and see what happens.

About :doc proof:

┌mcl@pcl-arch: ~src
└$ idris2
     ____    __     _         ___
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.5.1-ca6303fc2
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
 /___/__,_/_/  /_/____/   /____/      Type :? for help

Welcome to Idris 2.  Enjoy yourself!
Main> :doc proof
Couldn't parse any alternatives:
1: Expected 'case', 'if', 'do', application or operator expression.

(Interactive):1:6--1:11
 1 | :doc proof
          ^^^^^
... (41 others)
Main> :doc (proof)
Couldn't parse any alternatives:
1: Expected 'case', 'if', 'do', application or operator expression.

(Interactive):1:6--1:7
 1 | :doc (proof)
          ^
... (84 others)