Famous agda match pattern

Question

Rude i

check : UExpr -> Maybe Expr 

And I have a test term

 testTerm : UExpr 

I hope that check successful, after which I want to extract the resulting Expr and manipulate it further. Mostly

 realTerm : Expr just realTerm = check testTerm 

So this definition would not get typecheck if check testTerm turned out to be nothing . Is it possible?

Answer 1

The usual deal is to write something like

 Just : {X : Set} -> Maybe X -> Set Just (just x) = One -- or whatever you call the fieldless record type Just nothing = Zero justify : {X : Set}(m : Maybe X){p : Just m} -> X justify (just x) = x justify nothing {()} 

If m calculates success, the type p is One, and the value is printed.

Answer 2

Well, I found one way to do this, which is kind of freaky and magical.

 testTerm-checks : Σ Expr (\e -> check testTerm ≡ just e) testTerm-checks = _ , refl realTerm : Expr realTerm = proj₁ testTerm-checks 

It gives me jeebies heebie, but not necessarily bad. Still interested in other ways.