Search Results
| Search type | Search syntax |
|---|---|
| Tags | [tag] |
| Exact | "words here" |
| Author |
user:1234 user:me (yours) |
| Score |
score:3 (3+) score:0 (none) |
| Answers |
answers:3 (3+) answers:0 (none) isaccepted:yes hasaccepted:no inquestion:1234 |
| Views | views:250 |
| Code | code:"if (foo != bar)" |
| Sections |
title:apples body:"apples oranges" |
| URL | url:"*.example.com" |
| Saves | in:saves |
| Status |
closed:yes duplicate:no migrated:no wiki:no |
| Types |
is:question is:answer |
| Exclude |
-[tag] -apples |
| For more details on advanced search visit our help page | |
Results tagged with agda
Search options questions only
not deleted
user 28
For questions regarding Agda: the programming language / proof assistant.
8
votes
1
answer
159
views
Are `P x` and `▸ ((next P) ⊛ (next x))` equivalent in Guarded Cubical Agda?
In Guarded Cubical Agda there's ▹_ : Set i → Set i and ▸_ : ▹ Set i → Set i.
If I've got P : X -> Set and x : X, are P x and ▸ ((next P) ⊛ (next x)) equivalent? …
- 1,001
5
votes
1
answer
183
views
Strictly-monotone "max" operation for constructive Brouwer-trees?
The Setting
I'm trying to use Agda's well-founded ordering to prove that something is terminating using Brouwer Trees i.e.
data Ord where
zero : Ord
succ : Ord -> Ord
limit : (Nat -> Ord) -> Ord …
- 1,001
9
votes
1
answer
365
views
Case splitting with quotient types in Cubical Agda
I'm getting started with Cubcal Agda and I'm quite confused. …
- 1,001
6
votes
1
answer
255
views
Parameterized Datatypes in a Universe à la Tarski?
I'm mechanizing the model in Agda, but I'm trying to abstract over the defined inductive types, so that I know my mechanization works for any set of inductive types. …
- 1,001
4
votes
2
answers
322
views
Reasoning about CwFs in a proof assistant
I've been chatting with folks on Mastodon about this but the perspective there is markedly Agda-focused, so I thought I'd ask here for some broader opinions. … In Agda, (1) and (2) are at odds with each other: there's the REWRITING option, but it doesn't support rewriting in terms of fields of a record. …
- 1,001