Questions tagged [agda]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
0
votes
2answers
46 views

Propositional truncation of excluded middle

It is clear to me that it should be impossible to prove : exclMidl = isProp A → ((A) ⊎ (¬ A)) Because it would give deciding oracle for every Proposition. My ...
1
vote
0answers
31 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
71 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
59 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
99 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
90 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 ...
4
votes
1answer
144 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 ...