~dannypsnl/violet

A programming language, half theorem prover

16c6071 nix flake update

28 days ago

cb3acc0 nix flake update

a month 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