Jacques Carette
Jacques Carette
Right - this is where we desperately need theories. Constraints are then (relational) axioms on the variables of that theory. Note that we could re-add some of the vocabulary of...
Lining up certain definitions is indeed a good idea.
My "best guess" would be that we want to see the types whenever it's not `Real`, at least as a first approximation. If the units make it clear what type...
As to your questions: - A single constructor to embed a `Clif` into an `Expr` is better - Let's wait on that design. It will be easiest to figure out...
Arrays already exist -- in the backend. They are "implementation structures". We don't need to talk about them at the theory / specification stage. If you start trying to implement...
The latest commit is a nice way to track down everything that needs to be touched.
The type checking errors is because... things are currently broken! Our use of vectors is quite bad, i.e. type incorrect. And there was no point in fixing it in the...
While I agree that working directly in Drasil is difficult, shaking out the design will only be possible within the full Drasil. Until it proves too difficult, I think it...
> Does it make sense to be using strings to represent variable-length dimensions for vectors (and other clifs)? I followed closely to how variables were defined in other parts of...
The current type system does not yet support dependent types, because it had no reason to. I guess it will very soon. Let @balacij handle that part. @balacij : our...