Skip to content

Commit c7bf582

Browse files
committed
more notes
1 parent 0074118 commit c7bf582

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

NOTES.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,8 @@ Notes and questions on the ongoing implementation of `agda2lambox`.
4343

4444
- How would we make it easier to do the plumbing from inside Agda?
4545

46+
- How to generate an actual file from CertiCoq-WASM or CertiCoq-Rust?
47+
4648
[ctorblocks]: https://github.com/MetaCoq/metacoq/blob/v1.3.1-8.19/erasure/theories/EConstructorsAsBlocks.v
4749
[envflags]: https://github.com/MetaCoq/metacoq/blob/ea3ed3c4b0d05508ce744f17a56c880c5f47c816/erasure/theories/EWellformed.v#L55
4850

0 commit comments

Comments
 (0)