HARD: Math unit error checking

ClemsonRSRG / RESOLVE

RESOLVE (REusable SOftware Language with VErification) is a specification and programming language designed for verifying correctness of object oriented programs.

https://www.cs.clemson.edu/resolve/

BSD 3-Clause "New" or "Revised" License

24 stars 16 forks source link

HARD: Math unit error checking #449

Open M-Sitaraman opened 3 months ago

M-Sitaraman commented 3 months ago

Proper formulation of inductive definition checking

yushan87 commented 3 months ago

@M-Sitaraman If my memory doesn't fail me, the current math type system does not type check the right hand side of any definition. Something wasn't working quite right with it, but it might be very hard to fix it.