在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,并推断出该值.