search

MonoidalAttackTrees / ILL-Impl

Implementation of a term assignment for intuitionistic linear logic
0 stars 0 forks source link

ILL-Impl Tensor Term vs Type #10

Closed tattymennis closed 8 years ago

tattymennis commented 8 years ago

a (X) b is a term that can be evaluated. However, the type rules show that a (X) b : T1 (X) T2. Does the language need a Tensor type (as I have implemented TensorTy and Tensor term term in Syntax)?

heades commented 8 years ago

Yes, there will need to be both a tensor term and a tensor type.

tattymennis commented 8 years ago

Great, I have that implemented. I called our (-o) Lolly for lack of a better name. I just have Lolly and TensorTy as the only types in the language. Are there any types I'm missing?

heades commented 8 years ago

Yeah, you are missing I the unit type.

On Jun 28, 2016, at 4:02 PM, Matthew Tennis notifications@github.com wrote:

Great, I have that implemented. I called our (-o) Lolly for lack of a better name. I just have Lolly and TensorTy as the only types in the language. Are there any types I'm missing?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/MonoidalAttackTrees/ILL-Impl/issues/10#issuecomment-229165350, or mute the thread https://github.com/notifications/unsubscribe/ABZ7mPPgmKmBMT5cPaWctRAOQo6-fOfmks5qQX3LgaJpZM4JAddu.

tattymennis commented 8 years ago

That's right. UnitTy has been included. This issue can be closed.

heades commented 8 years ago

That's right. UnitTy has been included. This issue can be closed.

Great! Nice work.