Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Rename homo to ∙-homo in Algebra.Morphism.Structures #2464

Open
wants to merge 12 commits into
base: master
Choose a base branch
from
Open

Rename homo to ∙-homo in Algebra.Morphism.Structures #2464

wants to merge 12 commits into from

Commits on Aug 29, 2024

  1. fixes agda#2458

    @jamesmckinna
    jamesmckinna committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    9d310ab View commit details
    Browse the repository at this point in the history

  2. caught two missing uses

    @jamesmckinna
    jamesmckinna committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    30c2880 View commit details
    Browse the repository at this point in the history

  3. caught two more missing uses

    @jamesmckinna
    jamesmckinna committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    bb55206 View commit details
    Browse the repository at this point in the history

  4. hopefully the last occurrences

    @jamesmckinna
    jamesmckinna committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    f04ff44 View commit details
    Browse the repository at this point in the history

Commits on Sep 3, 2024

  1. Merge branch 'master' into issue2458

    @jamesmckinna
    jamesmckinna authored Sep 3, 2024
    Configuration menu
    Copy the full SHA
    f7bb1d6 View commit details
    Browse the repository at this point in the history

  2. fix indentation; what about the deprecation?

    @jamesmckinna
    jamesmckinna committed Sep 3, 2024
    Configuration menu
    Copy the full SHA
    11e0363 View commit details
    Browse the repository at this point in the history

Commits on Sep 4, 2024

  1. last occurrence of homo; plus indentation...

    @jamesmckinna
    jamesmckinna committed Sep 4, 2024
    Configuration menu
    Copy the full SHA
    54add53 View commit details
    Browse the repository at this point in the history

  2. more indentation...

    @jamesmckinna
    jamesmckinna committed Sep 4, 2024
    Configuration menu
    Copy the full SHA
    6184200 View commit details
    Browse the repository at this point in the history

Commits on Dec 7, 2024

  1. Merge branch 'agda:master' into issue2458

    @jamesmckinna
    jamesmckinna authored Dec 7, 2024
    Configuration menu
    Copy the full SHA
    d9921ed View commit details
    Browse the repository at this point in the history

  2. fix imports at top-level and exports from KleeneAlgebraHomomorphism

    @jamesmckinna
    jamesmckinna committed Dec 7, 2024
    Configuration menu
    Copy the full SHA
    7fb2d88 View commit details
    Browse the repository at this point in the history

Commits on Dec 9, 2024

  1. Merge branch 'agda:master' into issue2458

    @jamesmckinna
    jamesmckinna authored Dec 9, 2024
    Configuration menu
    Copy the full SHA
    8ca873f View commit details
    Browse the repository at this point in the history

  2. knock-on

    @jamesmckinna
    jamesmckinna committed Dec 9, 2024
    Configuration menu
    Copy the full SHA
    a566644 View commit details
    Browse the repository at this point in the history