Features priorities

[lemastero]

Assumption: We want to have readable Rust output (support subset of Agda not everything)

Here are tentative priority of features to be added:

• data types: support product types using struct

struct Person {
    name: String,
    age: u8,
}

• use Rust tuples for build in Data.Product
• pattern matching using match
• multiple arguments
• Agda records without implementations should be Rust traits - new pragma
• handle polymorphic functions (polymorphic identity) using Rust Generics
• recursive definitions like Nat (need example), TODO need Rust example
• expand support for sum types to handle enums with parameters
• expressions (Bool, =, Nat, Z - handled using build in Rust types), see Rust expressions
• currying
• assignment to single type (Set) as alias
• translate (some) Agda instances into Generic Bounds
• how to express basic Rust types: i8, i16, i32, i64, i128, u8, u16, u32, u64, u128? do we need new Agda library
• how to treat Strings - perhaps List Data.Char / Data.String treat both as rust strings?
• handle borrow and ownership for String / Vec
• pragmas for modules / functions visibilities