Stream: math-comp users

Topic: Printing finmap's allpairs forgets notation

view this post on Zulip Ana de Almeida Borges (Mar 28 2023 at 17:03):

Hi. I just discovered some unexpected behavior when printing an allpairs defined with finmap:

From mathcomp Require Import all_ssreflect finmap.
Open Scope fset.

Definition fine (xs : {fset nat}) := [fset y | y in 'I_3, x in xs].
Print fine.
fine =
fun xs : {fset nat} => [fset y | y in 'I_3,_ in xs]
     : {fset nat} -> {fset ordinal_choiceType 3}

Arguments fine xs

Definition weird (xs : {fset nat}) := [fset y | x in xs, y in 'I_3].
Print weird.
weird =
fun xs : {fset nat} =>
Imfset.imfset2 imfset_key (K:=ordinal_choiceType 3) (T1:=nat_choiceType)
  (T2:=fun=> ordinal_choiceType 3) (fun x : nat_choiceType => id)
  (p1:=mem_fin (fin_finpred (pT:=fset_finpredType nat_choiceType) xs))
  (p2:=fun x0 : nat_choiceType =>
         (fin_finpred (pT:=pred_finpredType (ordinal_finType 3)) ((fun=> 'I_3) x0)))
  (Phantom (mem_pred nat_choiceType) (mem xs))
  (Phantom (nat_choiceType -> mem_pred 'I_3)
     (fun x0 : nat_choiceType => mem ((fun=> 'I_3) x0)))
     : {fset nat} -> {fset ordinal_choiceType 3}

Arguments weird xs

Note how the printing is beautiful when the first variable ranges over 'I_3 but ugly when the second variable does. This doesn't happen if instead of 'I_3 I write, say, ys. Is it a bug, or is it somehow unavoidable?

Last updated: Jul 15 2024 at 20:02 UTC