Skip to content

Conversation

@gares
Copy link
Member

@gares gares commented Aug 13, 2020

No description provided.

gares added 2 commits August 13, 2020 15:11
Accessible via the following attributes
- #[mathcomp] enable generation of compat code
- #[mathcomp(axiom="axiom_name")] when the new mixin consists of
  exactly one axiom
@gares
Copy link
Member Author

gares commented Aug 13, 2020

IDEA to "simplify" the phant- business:

  • a DSL with under N T x\ and phunif M L R Rest and end BO constructors
  • an interpreter running the current phant-blabla code in the right context of decl

@gares
Copy link
Member Author

gares commented Aug 26, 2020

merged as part of #109

@gares gares closed this Aug 26, 2020
@gares gares deleted the mathcomp-compat branch October 8, 2023 13:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants