[Agda] forced arguments in EqReasoning

[James Wood]

On 28/11/2020 16:03, mechvel at scico.botik.ru wrote:
> Also James Wood writes that the definition of =fr (and thus =fr' too) 
> ignore certain
> parts of the Fraction record (the two remaining fields), and so the 
> unification will
> not work in  =fr
> (if so, then probably for =fr' too).
> ?
In reply to the parenthetical remark, precisely not. With `record` or 
`data`, it is fine, because those definitions do not compute 
automatically. This is the key part of Sandro's _≃_ example. I think, in 
fact, exactly the same thing is happening in that example (fields being 
missed).

 > The point of the record is for Agda to remember the two parameters f
 > and g, which it 'forgets' when you provide a value of the defined
 > equality type directly.

James