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

Question

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:

• Given Is-just m and Is-nothing m, how to eliminate? Can Relation.Nullary.Negation.contradiction be used here?
• Given a property p : ... → (mp : Is-just m) → ... → ... ≡ to-witness mp that needs to be shown inductively by p ... = {! p ... (subst Is-just m≡somethingelse mp) ... !}, the given term does not fill the hole, because it has type ... ≡ to-witness (subst Is-just m≡somethingelse mp).

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

Answer 1

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.