[Agda] How does one debug a programme that one has proved correct?
Ulf Norell
ulf.norell at gmail.com
Fri May 4 22:16:39 CEST 2018
You can clone the Agda repo at https://github.com/agda/agda. I was using
the `stable-2.5`
branch, but I would expect `master` to work the same (the difference is
@saizan's cubical
type theory goodness which is only on master). It should (fingers crossed)
build and install
with `make install-bin` or even `cabal install`.
/ Ulf
On Fri, May 4, 2018 at 10:03 PM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:
> Thanks, Ulf! How do I get the most recent development version? It sounds
> like that might resolve my problem. Although understanding what went wrong
> would still be very helpful indeed, so I would be most appreciative if you
> could look into it.
>
> Thanks for pointing out that the definition was wrong. I've fixed the
> definition of plus in the repository, so you won't have to contend with the
> indignity of (plus two two) yielding two rather than four.
>
> Cheers, -- P
>
> . \ Philip Wadler, Professor of Theoretical Computer Science,
> . /\ School of Informatics, University of Edinburgh
> . / \ and Senior Research Fellow, IOHK
> . http://homepages.inf.ed.ac.uk/wadler/
>
> On 4 May 2018 at 16:30, Ulf Norell <ulf.norell at gmail.com> wrote:
>
>> Something is indeed strange. Some observations:
>>
>> - _x_1862 is an unsolved metavariable. If I paste in the term in your
>> example there
>> is indeed some yellow. When printing a term Agda hides all implicit
>> arguments without
>> regard for whether they can actually be inferred (since this is
>> impractical to figure out).
>> This means that you often cannot take a printed term and type check it
>> without ending
>> up with some yellow.
>>
>> - On recent development Agda I can normalise (C-c C-n) `normalise 15
>> ⊢four`
>> in a handful of milliseconds. (It requires 15 fuel, and since you
>> forgot the Suc
>> in the recursive case of ⊢plus, normalises to two instead of four).
>> However, trying to prove that it reaches a normal form I get stuck:
>>
>> IsNormal : ∀ {M A} {⊢M : ε ⊢ M ⦂ A} → Normalise ⊢M → Set
>> IsNormal (out-of-gas _ _) = ⊥
>> IsNormal (normal _ _ _) = ⊤
>>
>> prf : IsNormal (normalise 15 ⊢four)
>> prf = tt -- does not come back
>>
>> On the other hand the following variant works fine:
>>
>> prf' : IsNormal (normalise 15 ⊢four) ≡ ⊤
>> prf' = refl -- checks in no time
>>
>> It's all very mysterious. I'll investigate deeper when I get a chance.
>>
>> / Ulf
>>
>> On Fri, May 4, 2018 at 7:44 PM, Philip Wadler <wadler at inf.ed.ac.uk>
>> wrote:
>>
>>> I have an Agda formalisation of reduction on raw terms (inspired by a
>>> formalisation of McBride acting on a deBruijn representation). The
>>> formalisation is here:
>>>
>>> https://wenkokke.github.io/sf/TypedFresh
>>>
>>> Although more elaborate than I would like in parts, at least I succeed
>>> in proving progress and preservation for the system. Combining the two
>>> allows me to write a function that computes the reduction sequence for a
>>> term bounding by a given length. If the reduction sequence is longer than
>>> the specified length n, it returns the sequence of length n with the
>>> indicator "out of gas". I then tried to compute the reduction sequence for
>>> two plus two.
>>>
>>> Computing the first four reduction steps takes a couple of minutes
>>> rather than a couple of seconds. Attempting to normalise the term fully
>>> (which should take fourteen reduction steps) does not complete even if run
>>> overnight!
>>>
>>> {-
>>> _ : normalise 4 ⊢four ≡
>>> out-of-gas
>>> ((`Y
>>> (`λ 0 ⇒
>>> (`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
>>> · (`suc (`suc `zero))
>>> · (`suc (`suc `zero))
>>> ⟶⟨ ξ-·₁ (ξ-·₁ (β-Y Fun refl)) ⟩
>>> (`λ 0 ⇒
>>> (`λ 1 ⇒
>>> `if0 ` 0 then ` 1 else
>>> (`Y
>>> (`λ 0 ⇒
>>> (`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
>>> · (`pred ` 0)
>>> · ` 1))
>>> · (`suc (`suc `zero))
>>> · (`suc (`suc `zero))
>>> ⟶⟨ ξ-·₁ (β-⇒ (Suc (Suc Zero))) ⟩
>>> (`λ 0 ⇒
>>> `if0 `suc (`suc `zero) then ` 0 else
>>> (`Y
>>> (`λ 1 ⇒
>>> (`λ 2 ⇒ (`λ 3 ⇒ `if0 ` 2 then ` 3 else ` 1 · (`pred ` 2) · ` 3))))
>>> · (`pred (`suc (`suc `zero)))
>>> · ` 0)
>>> · (`suc (`suc `zero))
>>> ⟶⟨ β-⇒ (Suc (Suc Zero)) ⟩
>>> `if0 `suc (`suc `zero) then `suc (`suc `zero) else
>>> (`Y
>>> (`λ 0 ⇒
>>> (`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
>>> · (`pred (`suc (`suc `zero)))
>>> · (`suc (`suc `zero))
>>> ⟶⟨ β-if0-suc (Suc Zero) ⟩
>>> (`Y
>>> (`λ 0 ⇒
>>> (`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
>>> · (`pred (`suc (`suc `zero)))
>>> · (`suc (`suc `zero))
>>> ∎)
>>> _ = refl
>>> -}
>>>
>>> To try to uncover the problem, I attempted a single step at a time. The
>>> first reduction step is fine.
>>>
>>> {-
>>> _ : normalise 1 ⊢four ≡
>>> out-of-gas
>>> ((`Y
>>> (`λ 0 ⇒
>>> (`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
>>> · (`suc (`suc `zero))
>>> · (`suc (`suc `zero))
>>> ⟶⟨ ξ-·₁ (ξ-·₁ (β-Y Fun refl)) ⟩
>>> (`λ 0 ⇒
>>> (`λ 1 ⇒
>>> `if0 ` 0 then ` 1 else
>>> (`Y
>>> (`λ 0 ⇒
>>> (`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
>>> · (`pred ` 0)
>>> · ` 1))
>>> · (`suc (`suc `zero))
>>> · (`suc (`suc `zero))
>>> ∎)
>>> (⊢λ
>>> (⊢λ
>>> (⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z)
>>> (⊢Y
>>> (⊢λ
>>> (⊢λ
>>> (⊢λ
>>> (⊢if0 (Ax (S m≢n Z)) (Ax Z)
>>> (Ax (S p≢n (S p≢m Z)) · ⊢pred (Ax (S m≢n Z)) · Ax Z)))))
>>> · ⊢pred (Ax (S (fresh-lemma CollectionDec.here) Z))
>>> · Ax Z)))
>>> · ⊢suc (⊢suc ⊢zero)
>>> · ⊢suc (⊢suc ⊢zero))
>>> _ = refl
>>> -}
>>>
>>> The second reduction step yields a huge term. It contains the free
>>> variable _x_1862 where I would have expected a fresh variable name to be
>>> computed. Looking at the four-step reduction above we see the name computed
>>> properly, but when going from the first step to the second it is not. The
>>> huge size of the type derivation suggests why it did not terminate after
>>> one day.
>>>
>>> Help! Why doesn’t the term reduce? Is there some way to force it to
>>> reduce?
>>>
>>> Cheers, -- P
>>>
>>> {-
>>> _ : normalise 1
>>> (⊢λ
>>> (⊢λ
>>> (⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z)
>>> (⊢Y
>>> (⊢λ
>>> (⊢λ
>>> (⊢λ
>>> (⊢if0 (Ax (S m≢n Z)) (Ax Z)
>>> (Ax (S p≢n (S p≢m Z)) · ⊢pred (Ax (S m≢n Z)) · Ax Z)))))
>>> · ⊢pred (Ax (S (fresh-lemma CollectionDec.here) Z))
>>> · Ax Z)))
>>> · ⊢suc (⊢suc ⊢zero)
>>> · ⊢suc (⊢suc ⊢zero))
>>> ≡
>>> out-of-gas
>>> ((`λ _x_1862 ⇒
>>> (`λ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ⇒
>>> `if0 ` _x_1862 then
>>> ` (suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)) else
>>> (`Y
>>> (`λ 0 ⇒
>>> (`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
>>> · (`pred ` _x_1862)
>>> · ` (suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005))))
>>> · (`suc (`suc `zero))
>>> · (`suc (`suc `zero))
>>> ⟶⟨ ξ-·₁ (β-⇒ (Suc (Suc Zero))) ⟩
>>> (`λ
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))
>>> ⇒
>>> `if0
>>> (((λ w →
>>> ((λ x → ` x) , _x_1862 ↦ `suc (`suc `zero)) w | w ≟ _x_1862)
>>> , suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↦
>>> `
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> _x_1862
>>> | _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
>>> then
>>> (((λ w →
>>> ((λ x → ` x) , _x_1862 ↦ `suc (`suc `zero)) w | w ≟ _x_1862)
>>> , suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↦
>>> `
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> (suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
>>> | suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
>>> else
>>> (`Y
>>> (`λ
>>> suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))
>>> ⇒
>>> (`λ
>>> suc
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⇒
>>> (`λ
>>> suc
>>> (suc
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
>>> ⊔
>>> (suc
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
>>> ⇒
>>> `if0
>>> `
>>> (suc
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
>>> then
>>> `
>>> (suc
>>> (suc
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
>>> ⊔
>>> (suc
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))))
>>> else
>>> `
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ·
>>> (`pred
>>> `
>>> (suc
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))))
>>> ·
>>> `
>>> (suc
>>> (suc
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
>>> ⊔
>>> (suc
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> (suc
>>> (foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> ⊔
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬?
>>> (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))))))))
>>> ·
>>> (`pred
>>> (((λ w →
>>> ((λ x → ` x) , _x_1862 ↦ `suc (`suc `zero)) w | w ≟ _x_1862)
>>> , suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↦
>>> `
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> _x_1862
>>> | _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> ·
>>> (((λ w →
>>> ((λ x → ` x) , _x_1862 ↦ `suc (`suc `zero)) w | w ≟ _x_1862)
>>> , suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↦
>>> `
>>> foldr _⊔_ 0
>>> (map suc
>>> (filter (λ x → ¬? (x ≟ _x_1862))
>>> (filter
>>> (λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> (_x_1862 ∷
>>> [ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
>>> | ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
>>> (suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005))
>>> | suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ≟
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
>>> · (`suc (`suc `zero))
>>> ∎)
>>> (⊢λ
>>> (⊢if0
>>> (.Typed.⊢ρ′
>>> (λ {w} w∈ {z₁} y∈ →
>>> .Typed.Σ
>>> (⊢λ
>>> (⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
>>> (⊢suc (⊢suc ⊢zero)) w∈ y∈
>>> | w ≟ _x_1862)
>>> (.Typed.⊢ρ
>>> (⊢λ
>>> (⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
>>> (⊢suc (⊢suc ⊢zero)))
>>> (λ {_} x∈ → x∈)
>>> (⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016)
>>> (CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈) CollectionDec.here
>>> | _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
>>> (S (fresh-lemma CollectionDec.here) Z)
>>> | _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
>>> (.Typed.⊢ρ′
>>> (λ {w} w∈ {z₁} y∈ →
>>> .Typed.Σ
>>> (⊢λ
>>> (⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
>>> (⊢suc (⊢suc ⊢zero)) w∈ y∈
>>> | w ≟ _x_1862)
>>> (.Typed.⊢ρ
>>> (⊢λ
>>> (⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
>>> (⊢suc (⊢suc ⊢zero)))
>>> (λ {_} x∈ → x∈)
>>> (⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016)
>>> (CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈)
>>> (CollectionDec.there CollectionDec.here)
>>> | suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
>>> Z
>>> | suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
>>> suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
>>> (⊢subst
>>> (λ {w} w∈′ {z₁} →
>>> .Typed.Σ′
>>> (λ {w₁} w∈ {z₂} y∈ →
>>> .Typed.Σ
>>> (⊢λ
>>> (⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
>>> (⊢suc (⊢suc ⊢zero)) w∈ y∈
>>> | w₁ ≟ _x_1862)
>>> (.Typed.⊢ρ
>>> (⊢λ
>>> (⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
>>> (⊢suc (⊢suc ⊢zero)))
>>> (λ {_} x∈ → x∈)
>>> (⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016) w∈′
>>> | w ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
>>> (.Typed.⊢ρ′
>>> (λ {w} w∈ {z₁} y∈ →
>>> .Typed.Σ
>>> (⊢λ
>>> (⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
>>> (⊢suc (⊢suc ⊢zero)) w∈ y∈
>>> | w ≟ _x_1862)
>>> (.Typed.⊢ρ
>>> (⊢λ
>>> (⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
>>> (⊢suc (⊢suc ⊢zero)))
>>> (λ {_} x∈ → x∈)
>>> (⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
>>> (λ {z₁} x →
>>> CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈)
>>> (CollectionDec.there (CollectionDec.there x))
>>> | z₁ ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
>>> _2016))
>>> · ⊢suc (⊢suc ⊢zero))
>>> -}
>>>
>>>
>>>
>>>
>>> . \ Philip Wadler, Professor of Theoretical Computer Science,
>>> . /\ School of Informatics, University of Edinburgh
>>> . / \ and Senior Research Fellow, IOHK
>>> . http://homepages.inf.ed.ac.uk/wadler/
>>>
>>> The University of Edinburgh is a charitable body, registered in
>>> Scotland, with registration number SC005336.
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>>
>>
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180504/ac7977fc/attachment.html>
More information about the Agda
mailing list