Skip to content

Conversation

JacquesCarette
Copy link
Contributor

Renames the functions, but not the syntax.

@MatthewDaggitt
Copy link
Contributor

Sorry, for not replying earlier. I have replied on the issue for how to rename the syntax.

@JacquesCarette
Copy link
Contributor Author

Thanks - hopefully I'll have time (and wifi) on the long train ride tomorrow to deal with this.

Copy link
Contributor

@jamesmckinna jamesmckinna left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

i think that following @MatthewDaggitt 's suggestions regarding syntax declarations, the following should do the trick instead of your renaming directive:

module ≤-Reasoning where
  import Relation.Binary.Reasoning.Base.Triple
    ≤-isPreorder
    <-trans
    <-resp-≃
    <⇒≤
    <-≤-trans
    ≤-<-trans
    as Triple
  open Triple public hiding (step-≈; step-≈˘)

  infixr 2 step-≃ step-≃˘
  step-≃  = Triple.step-≈
  step-≃˘ = Triple.step-≈˘
  
  syntax step-≃  x y∼z x≃y = x ≃⟨  x≃y ⟩ y∼z
  syntax step-≃˘ x y∼z y≃x = x ≃˘⟨ y≃x ⟩ y∼z

with this a model for any subsequent downstream changes which may be required.

EDITED The 'problem' with a mere renaming /why it does not work, is that the syntax declaration and the infixes are declared in a different scope, and then agda's parser complains... so one needs to be more belt-and-braces about redeclaring the names, their infix status, and their syntax... groan.

@jamesmckinna
Copy link
Contributor

superseded now by #1916

@MatthewDaggitt MatthewDaggitt added status: duplicate The main contents of the issue or PR already exists in another issue or PR. and removed status: being-worked-on labels Jan 26, 2023
@MatthewDaggitt MatthewDaggitt deleted the Issue1437 branch January 26, 2023 07:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug naming status: duplicate The main contents of the issue or PR already exists in another issue or PR.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants