creating a pair in term mode

Stream: general

[Filippo A. E. Nuccio]

I am trying to golf the following proof

begin
  constructor,
  intros F s,
  use ⟨(λ _, F s), (λ _, F.2 s)⟩,
end

to term mode. I would have expected something like

λ F s, ⟨(λ _, F s), (λ _, F.2 s)⟩

but it does not work (clearly, the object I am constructing is part of a structure which has two components). How do I construct a pair in term mode?

[Chris Hughes]

Without knowing the expected type I can't tell you exactly what to do, but probably wrapping the entire proof in angle brackets will work.

[Yaël Dillies]

A pair as in a term of α × β? If so, it's (a, b)

[Yaël Dillies]

But if it's a structure then yeah more angle brackets should do it.

[Filippo A. E. Nuccio]

It's a structure, and I have tried inserting a lot of angle brackets indeed. I was wondering if there is a " general dictionary", but I think it is probably too long to explain the details here.

[Filippo A. E. Nuccio]

I will try to come up with a MWE if needed, thanks

[Reid Barton]

The term you wrote corresponds to your tactic proof with the first constructor deleted

[Filippo A. E. Nuccio]

Ah, so something like

⟨λ F s, ⟨(λ _, F s), (λ _, F.2 s)⟩⟩

should work....

[Filippo A. E. Nuccio]

It does! Thanks :octopus:

[Filippo A. E. Nuccio]

I had not tried putting the angle brackets so far outside

[Johan Commelin]

@Filippo A. E. Nuccio constructor breaks open the structure. In term mode, it corresponds to a pair of pointy angle brackets (-;

[Filippo A. E. Nuccio]

Thanks!