Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [agda]

The tag has no usage guidance.

1
vote
0answers
24 views

Strict Positivity of Indexed Datatype in Agda

Agda is ruling out definitions like data Bad : Set where bad : (Bad → Bad) → Bad Because "Non strictly-positive declarations are rejected because one can write ...
4
votes
1answer
51 views

Proof that type does not have decidable equality in Agda

Can one create such function in Agda ? ℕ→ℕ-undecidable : ¬ ( (f g : ℕ → ℕ ) → Dec (f ≡ g)) ℕ→ℕ-undecidable = ? I am particularly interested in proof using ...
2
votes
1answer
53 views

Can one get Turing-completeness without nontermination?

As I'm reading the movfuscator paper by Stephen Dolan, I encounter this claim: In order to have Turing-completeness, we must allow for nontermination. This seems like a reasonable statement. But I'...
2
votes
1answer
86 views

Why this pattern matching fails in Agda?

Consider function wa'' (need natural number definition, either in stdlib or Agda.Builtin.Nat): ...
3
votes
2answers
76 views

In Agda's GADT, is “parameterized” and “indexed” different semantically?

I know they have difference in scoping: data a (n : Set) : Set where introA : a n data b : Set -> Set where introB : {n : Set} -> b n That's not ...
3
votes
1answer
126 views

What does it mean if we disable K-rule in Agda?

TL;DR: Can I say, "K-rule in Agda enables people to match $ \forall a.a \equiv a $ with $ refl $"? In https://agda.readthedocs.io/en/v2.5.4.1/language/without-k.html#without-k, K-rule is introduced ...