haskell - agda 中的已知模式匹配

Question

大致上，我有

check : UExpr -> Maybe Expr

我有一个测试术语

testTerm : UExpr

我希望会 check成功，之后我想提取结果 Expr并进一步操纵它。基本上

realTerm : Expr
just realTerm = check testTerm

这样，如果 check testTerm，此定义将无法进行类型检查原来是 nothing .这可能吗？

Answer 1

通常的交易是写类似的东西

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 {()}

如果 m 计算成功，则 p 的类型为 One，并推断出值。