pp.all with more @

Stream: general

[Jason Rute]

I don't suppose there is a pretty printer that is even more ambitious with @'s, is there? For example, consider the pp.all version of theorem or.symm.equations._eqn_1:

@eq.{0} (∀ {a b : Prop}, or a b → or b a) or.symm or.swap

If you enter this into Lean it will give a "type mismatch" error. The trick is to enter it as follows:

@eq.{0} (∀ {a b : Prop}, or a b → or b a) @or.symm @or.swap

This is because or.symm has type or.symm : ∀ {a b : Prop}, a ∨ b → b ∨ a. Now, I think this is a minor bug and I if others agree can make an issue about it, but I also wonder if there is already a pretty printer that is more ambitious with the @ symbol. For example, it is ok to enter this as follows:

@eq.{0} (∀ {a b : Prop}, @or @a @b → @or @b @a) @or.symm @or.swap

(If you can't tell, I'm trying to take the pp.all output of Lean and plug it back in to Lean. Exceptions like this make it less than 100% robust.)

[Chris B]

I know the one I wrote for nanoda/nanoda_lib will do this if you send Local items through the Const formatter instead of just printing them directly. I disabled it because I thought it was ugly but it's an option. I think Trepplein's pretty printer does this with implicits enabled as well. I'll check when I'm back at my desktop.

[Chris B]

As for plugging pretty-printed terms back into Lean I think mine has an ~85% success rate but there are still some rough spots to grind down. I haven't spent much time on it but it's an interesting goal.

[Jason Rute]

Another related, but opposite issue is that sometimes pp.all adds @ where it shouldn't go. Here is an example:

set_option pp.all true
theorem id_defn : @id = (λ {α : Type} (x: α), x) := by refl
#check congr_fun id_defn bool -- @eq.{1} ((λ (x : Type), x → x) bool) (@id.{1} bool) (@(λ {α : Type} (x : α), x) bool)

If you try to plug the following into Lean

@eq.{1} ((λ (x : Type), x → x) bool) (@id.{1} bool) (@(λ {α : Type} (x : α), x) bool)

it will complain about an "invalid @" (the one before the lambda expression). Actually, I don't think it is possible to directly type this theorem into Lean, although you can type the definitionally equivalent theorem:

@eq.{1} ((λ (x : Type), x → x) bool) (@id.{1} bool) ((λ (α : Type) (x : α), x) bool)

where one replaces the braces in the lambda expression with parentheses.

[Chris B]

That one might be a bug. I just tested it with the nanoda one and got :

theorem id_defn : @id = (λ {α : Type} (x: α), x) := by refl
def jasons_def : _ :=congr_fun id_defn bool

-- pp output
lemma jasons_def : @eq (Π (a : @bool), @bool) (@id @bool)
    (λ (x : @bool), @x) :=
@congr_fun (Type 0) (λ (x : Type 0), Π (a : @x), @x) @id
  (λ {α : Type 0} (x : @α), @x) @id_defn @bool

[Chris B]

It did come out without parens around the first (Type 0) though.

[Mario Carneiro]

Yep, @(λ ...) is an issue with the parser. There is no concrete syntax for this, and the pretty printer is using a reasonable choice for what that syntax should be but the parser doesn't like it. Maybe we can fix this in lean 3.5.1?

[Chris B]

Ah that makes sense.

[Jason Rute]

Since this is becoming "issues with the pretty printer", here is another:

import system.random
set_option pp.all true
#check @rand_nat_aux._main._pack._wf_rec_mk_dec_tactic._aux_1

The resulting Prop has near the end, the bad names .nat, .nat.has_add, and .nat.has_one. Oddly enough, if one copies the theorem fixes the extra .s and puts it back into Lean, then it will pretty print it correctly. Maybe the issue is with the underlying expression.