Skip to content

Comments

Make the usage of field keyword consistent#658

Merged
carlostome merged 5 commits intomasterfrom
656-make-the-usage-of-field-keyword-consistent
Feb 6, 2025
Merged

Make the usage of field keyword consistent#658
carlostome merged 5 commits intomasterfrom
656-make-the-usage-of-field-keyword-consistent

Conversation

@williamdemeo
Copy link
Member

@williamdemeo williamdemeo commented Jan 30, 2025

Description

This closes issue #656

  • Remove all \begin{code}[hide] blocks surrounding occurrences of field keyword

  • Unhide record constructor bracket syntax definitions, since this was inconsistent (some constructor syntax definitions were hidden and some were not).

  • Make indentation convention for field names in lagda files consistent.

Checklist

  • Commit sequence broadly makes sense and commits have useful messages
  • Any semantic changes to the specifications are documented in CHANGELOG.md
  • Code is formatted according to CONTRIBUTING.md
  • Self-reviewed the diff

This closes issue #656

+ Remove all `\begin{code}[hide]` blocks surrounding occurrences of
  `field` keyword

+ Also unhide record constructor bracket syntax definitions, since this
  was inconsistent (some constructor definitions were hidden and some were not).
@williamdemeo williamdemeo linked an issue Jan 30, 2025 that may be closed by this pull request
@williamdemeo williamdemeo marked this pull request as ready for review January 30, 2025 18:39
@williamdemeo williamdemeo self-assigned this Feb 3, 2025
@williamdemeo williamdemeo requested review from WhatisRT and carlostome and removed request for WhatisRT and carlostome February 4, 2025 14:23
@williamdemeo williamdemeo marked this pull request as draft February 4, 2025 15:15
@williamdemeo williamdemeo marked this pull request as ready for review February 4, 2025 15:52
Copy link
Collaborator

@carlostome carlostome left a comment

Choose a reason for hiding this comment

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

Some nitpicks

@williamdemeo williamdemeo force-pushed the 656-make-the-usage-of-field-keyword-consistent branch from 57c818a to bc2dac5 Compare February 5, 2025 19:22
Copy link
Collaborator

@carlostome carlostome left a comment

Choose a reason for hiding this comment

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

LGTM!

@carlostome carlostome merged commit ebc1357 into master Feb 6, 2025
8 of 10 checks passed
@carlostome carlostome deleted the 656-make-the-usage-of-field-keyword-consistent branch February 6, 2025 08:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Make the usage of field keyword consistent

2 participants