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

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

Agda >=2.6.3 hangs on conflicting record directives · Issue #7301 · agda/agda · GitHub

Since 2.6.3, Agda hangs on:

record Foo : Set where
  inductive; coinductive

Agda-2.6.2 still says:

agda-2.6.2 ConflictingRecordDirectives.agda
/Users/abel/play/agda/bugs/ConflictingRecordDirectives.agda:2,3-3
/Users/abel/play/agda/bugs/ConflictingRecordDirectives.agda:2,3: Repeated record directives at:
/Users/abel/play/agda/bugs/ConflictingRecordDirectives.agda:2,3-12
/Users/abel/play/agda/bugs/ConflictingRecordDirectives.agda:2,14-25

<EOF><ERROR>
...

This was the behavior since 2.5.1.1.

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