HARD: Math unit error checking

rhit-csse-projects / 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

0 stars 0 forks source link

HARD: Math unit error checking #3

Open AdityaSenthilvel opened 2 months ago

AdityaSenthilvel commented 2 months ago

Proper formulation of inductive definition checking, Math unit errors: Definition type vs usage of is or =

Comment from Sami: 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. All Definition are assuming that there is no body due to type checking issues.

drholly77 commented 2 months ago

@rhit-csse-projects/t17-2425 Here is a resource for: what is an inductive definition A ~2 page excerpt from Chapter 5 from InductiveDefinitionBasics.pdf by Kenneth H. Rosen

drholly77 commented 2 months ago

@rhit-csse-projects/t17-2425 As of 27 Sept 2024, please ignore this issue We'll come back to it at a later date