Abstract operators

Stream: new members

[ziman]

I've got another question. I'm trying to define some custom operators but I don't think I'm doing this right.

import Init.Data.Nat.Basic

set_option autoImplicit false
set_option quotPrecheck false

variable {n : Nat}

structure A (n : Nat) : Type where
  nr : Fin n

def Rel (n : Nat) : Type := (A n × A n) → (A n × A n) → Prop

infix:36 " ≥_l " => ge

-- so far so good

def gt (ge : Rel n) : Rel n :=
  fun ab cd => (ab ≥_l cd) ∧ ¬(cd ≥_l ab)  -- ERROR HERE

notation:36 lhs " >_l " rhs => gt ge lhs rhs

-- MFE.lean:18:16
-- unknown identifier 'ge✝'

In Agda, I'd make the whole module parameterised by ge, and then refer to that. (Well, in Agda, I'd just name it _≥_ directly but that's not the point.) Since Lean is parameterised on a per-definition basis, there is no "global" ge so I disabled quotPrecheck and was trying to make $\ge_l$ to refer to whatever ge is in scope instead. But that's probably not a good idea because I'm getting an error.

I could add variable (ge : Rel n) but then I lose control over that parameter, as all references to $\ge_l$ start referring to ge✝ instead and I can't control where that parameter appears, whether it's implicit or explicit or so, and that's causing a whole set of problems of its own further down the line, so I've mostly stopped using section variables in my code.

How can I properly say "my development refers to an abstract greater-than-or-equal relation, written $\ge_l$", and then derive further operators from that?

[ziman]

Alright, it seems that adding set_option quotPrecheck.allowSectionVars true and variable (ge : Rel n), but no other unnecessary variables, does what I want. It seems to create ge✝ and refer to it just where I need it.

It seems I misunderstood the variable declaration. I thought it was just "please auto-quantify these names for me" but it seems to do more than that, creating the dagger variables and all that.

[ziman]

I'd delete my question but it seems it's not possible anymore.

[Robin Arnez]

You need

set_option hygiene false in
infix:36 " ≥_l " => ge

to make sure it doesn't refer to some ge._@.external:file:///MathlibDemo/MathlibDemo.lean._hyg.53

[ziman]

Ah, thank you! :)