Constantine Theocharis

icon indicating an email [email protected]

icon company University of St Andrews icon location UK icon location In pursuit of corectnes

Results 55 issues of Constantine Theocharis

Directive resolve: #use + #pure + #comptime + #unsafe

type-system

Function attribute struct

type-system

Syntax change: data type refinements

type-system

Implement proof search for `infer_term` for use types

type-system

Add proof irrelevance to data definitions

type-system

Elaborate implicit function calls and default arguments

This should happen after resolution, before typechecking. Elided arguments should be created as holes.

type-system

Add mechanism for declaring default data defs for unannotated literals.

For example, `x := 3` should default as `x: i32`.

type-system

Add discovery + resolution tests

type-system

Create an error store and keep errors there rather than pass-by-value

type-system

Function defs should record their captured variables if they are closures

This should probably be a different variant of FnBody

type-system