~dannypsnl/violet

A programming language, half theorem prover

3d8388f add expect_test, update formatter

14 days ago

e4e09ed nix flake update

2 months ago

#violet

This project redevelop violet but using nameful context (library Yuujinchou).

  • core unification and meta solving: elaboration-zoo
  • (TODO) term
    • local let
    • (?) first class sigma v.s. record based sigma
    • (?) elaborator operations
  • (TODO) top level
    • open statement
    • export keyword for top let
  • (TODO) inductive types
    • strictly positive check
    • (?) sized type for termination checker
  • (TODO) universe polymorphism: library mugen
  • (TODO) pattern matching