Sofia Rodrigues issues

Results 19 issues of


                                            Sofia Rodrigues

Make parenthesis non-obligatory inside return statement.

feature

Some functions and constructors should not be compiled to KDL

Some functions are present in the Kind2 genesis block thus they should not be compiled.

feature

Add an API for cursor on trees

Ability to walk inside the tree and apply tactics

feature

"New Type" Optimization

scope: optimization

Add type checker for erased Pi, App and Lam

feature

scope: type_checker

Improve error messages by removing things like implicit arguments

scope: developer experience

Move Item from lexeme to a new file

code: rewrite

Problem with relevance checking with type constructors

``` type Bool { true false } Fun (n: U60) : Type Fun _ = Bool Main : Type Main = Fun 2 ``` Does not triggers a relevance error.

status: confirmed bug

Problem with variables named `dup`

``` #derive[match] type Node { dup bup } ``` ``` thread 'main' panicked at 'Expected `name`: 880 | (Q$Node.match orig (Kind.Term.ct0 (Node.dup.) orig) motive dup bup) = (Kind.Term.ann 536870941 (Kind.Term.set_origin...

status: confirmed bug

Add Float Support

feature