CODEWITHSUNDEEP
agdaoption-type
Helmut Grohne
Helmut Grohne

Reputation: 6788

Is there any non-trivial code that uses Data.Maybe.Is-just?

The Agda standard library provides a data type Maybe accompanied with a view Any. Then there is the property Is-just defined using Any. I found working with this type difficult as the standard library provides exactly no tooling for Any.

Thus I am looking for examples on how to work with Is-just effectively. Is there an open source project that uses it?

Alternatively, I am seeking how to put it to good use:

Often it seems easier to work with Σ A (_≡_ m ∘ just) than Is-just m.

Upvotes: 2

Views: 129

Answers (1)

gallais
gallais

Reputation: 12113

Regarding your first question, it is possible to derive a contradiction from having both Is-just m and Is-nothing m in context. You can then use ⊥-elim to prove anything.

module isJust where

open import Level
open import Data.Empty
open import Data.Maybe

contradiction :
  {ℓ : Level} {A : Set ℓ} {m : Maybe A}
  (j : Is-just m) (n : Is-nothing m) → ⊥
contradiction (just _) (just pr) = pr

The second one is a bit too abstract for me to be sure whether what I'm suggesting will work but the usual strategies are to try to pattern match on the value of type Maybe A or on the proof that Is-just m.

As for using another definition of Is-just, I tend to like

open import Data.Bool

isJust : {ℓ : Level} {A : Set ℓ} (m : Maybe A) → Set
isJust m = T (is-just m)

because it computes.

Upvotes: 1

Related Questions