A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://github.com/agda/agda/issues/5299 below:

Postfix projections are not documented · Issue #5299 · agda/agda · GitHub

Skip to content Navigation Menu Search code, repositories, users, issues, pull requests...

Saved searches Use saved searches to filter your results more quickly

Sign up You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert

Postfix projections are not documented #5299

Assignees

Description

It seems the user manual is missing an explanation of postfix notation for record projections. Searching for postfix gives the flag --postfix-projections as the only result, but it does not actually explain the syntax anywhere.

andreasabel, jliptrap and axelf4

Metadata Metadata

Development

No branches or pull requests Issue actions

You can’t perform that action at this time.

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4