Open andrevidela opened 4 years ago
In src/PetriFormat.idr we use dropContext to update the type of our TDef which is used in a context with a greater arity than itself.
src/PetriFormat.idr
dropContext
typedefs/typedefs#221 Introduces the same function. When it is merged, we should remove ignoreWeaken in favor of the Typedefs implementation.
ignoreWeaken
In
src/PetriFormat.idrwe usedropContextto update the type of our TDef which is used in a context with a greater arity than itself.typedefs/typedefs#221 Introduces the same function. When it is merged, we should remove
ignoreWeakenin favor of the Typedefs implementation.