Franziskus Kiefer

I'm trying to get the p256 code into hacspec https://github.com/hacspec/hacspec/blob/927034252b93140099738075271c3ccc3daedc80/examples/p256/src/p256.rs#L71-L75

Thanks for tackling this. It is very much appreciated. A few pointers and historic context first. - There is a `Numeric` trait in `traits.rs` that should be used, extended, or...

The `Numeric` trait and work around it have been pretty ad-hoc. So getting a more thought out design in would be good. Those are great resources. Maybe the first task...

Hi @tanmay2004 what's the state of this PR? I think most typechecker related issues that we ran into here should be fixed by now.

Hi Milo, thanks for your interest in hacspec! Adding Coq as a compilation target would be great. If you have a `rustspec_to_coq.rs` file already, you can add it in a...

I really like the idea! Both actually, the first one is a little more realistic at this point though 😉 One question would be about the semantics of a `#[hacspec]`...

> either you change to `#[derive(Clone)] pub struct MyTupleType(...)`, and you get the `.clone()` function for free with the current typechecker (I think it should work) Ah... 🤦🏻 I forgot...

This should be supported. I consider this a bug in the typechecker. For now the workaround is to use tuple structs. But we should really fix this...

I ran into another instance of this. The unexpected error is thrown by the typechecker when trying to convert a `ByteSeq` into a `ChaChaPolyKey` (array). We have only a `use...

👍🏻 yes, we should put the code generation into a GH action. This will need some setup work that's necessary for running backend tests anyway. There's #154 that I meant...