如何解决为什么 Record 会忘记哪些参数是隐式的?
似乎当 Record 转换为 Variant 时,它会丢弃有关哪些参数是隐式的数据。为什么?这是一个 MWE:
> Variant example {n : nat} (e : n=n) :=
| a : nat -> example e.
> Check a.
a
: forall e : ?n = ?n,nat -> example e
where
?n : [ |- nat]
> Record example2 {n : nat} (e : n=n) := a2 { r: nat }.
> Check a2.
a2
: forall (n : nat) (e : n = n),nat -> example2 e
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。