[Agda] unfolding just a single definition in the context of a goal

[James Wood]

Hi Christian,

I believe the answer is unfortunately no. A feature to achieve this has
probably always seemed too difficult to design well and implement, so
it's never been done.

To practically achieve something similar, it's good to know how to do
type annotations. Generally, if you see something in the goal display
that you want to look different, you can annotate its type in the
program text and it'll appear like that in the goal display. If it's the
goal itself, annotation can be done via stdlib's Function.Base._∋_ :
  _∋_ : ∀ {a} (A : Set a) → A → A
  A ∋ x = x
If it's a variable (like in your example), you can create an alias of it
using `let`, e.g,
  sets-have-wconstant-≡-endomaps' : (X : Type ℓ) → is-set X →
                                    wconstant-≡-endomaps X
  sets-have-wconstant-≡-endomaps' X p =
    let p′ : (x y : X) → is-subsingleton (x ≡ y)
        p′ = p
    in {!!}
There's not really any way to automate this, but at least the type you
write down will be checked.

If you have control of the definitions, it can also sometimes be useful
to define types via records, rather than computing types. For example,
if `is-subsingleton` were defined as follows, `C-u C-u C-c C-,` would
give you the display you wanted.
  record is-subsingleton (X : Type ℓ) : Type ℓ where
    constructor mk
    field get : ∀ x y → Id X x y
  open is-subsingleton public
With this definition, expansion of the definition is effectively
controlled by the programmer's use of `mk` and `get`. I suppose it's a
matter of experience to know when it's worth making the trade-off
between manual and automatic expansion of definitions, and it also isn't
just about goal displays.

Hope that was helpful,
James

On 13/07/2020 14:31, Marcus Christian Lehmann wrote:
> Dear Agda community,
> 
> When in in context of a goal, Is there a way to have just one definition
> unfolded instead of a complete normalization that is performed on `C-u
> C-u C-c C-,` ?
> 
> For example: in the notes of M. Escardó [1] there is something like
> 
>   sets-have-wconstant-≡-endomaps' : (X : Type ℓ) → is-set X →
> wconstant-≡-endomaps X
>   sets-have-wconstant-≡-endomaps' X p = {!!}
> 
> Now, in the hole {!!}, whe using `C-c C-,` or `C-u C-c C-,`this gives a
> 
>   Goal: wconstant-≡-endomaps X
> ————————————————————————————————————————————————————————————
>   p : is-set X
>   X : Type ℓ
> 
> where `C-u C-u C-c C-,` normalizes all terms and gives
> 
>   Goal: (x y : X) →
>         Σ (λ f → (x₁ x' : Id X x y) → Id (Id X x y) (f x₁) (f x'))
> ————————————————————————————————————————————————————————————
>   p : (x y : X) (x₁ y₁ : Id X x y) → Id (Id X x y) x₁ y₁
>   X : Set ℓ
> 
> In this case my question is whether it is possible to have just one
> definition unfolded, e.g. just have `is-set` unfolded and get an
> intermediate result like
> 
>   Goal: wconstant-≡-endomaps X
> ————————————————————————————————————————————————————————————
>   p : (x y : X) → is-subsingleton (x ≡ y)
>   X : Type ℓ
> 
> I could not find any hints about that in the agda documentation.
> 
> kind regards,
> Christian
> 
> [1]
> https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#setscharacterization
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>