Replies: 2 comments 1 reply
-
The main question I have regarding this is: are there developments in F* out there already which use setoids? I am also interested how the design decisions play out with SMT. The closest thing I can think of are special notions of equality, like |
Beta Was this translation helpful? Give feedback.
-
Currently I'm experimenting with typeclass-based abstract algebra structures:
As you can see in ringlikes, proofs become easier to read when you use (+) and (*) to denote the operations. They can of course be made way less verbose if I introduce forall opaques like I did in my record-based abstract algebra implementation. I'm still unfamiliar with tactics, so I can't tell if I can perform trivial transformations with tactics when I use custom equivalence relation -- if anyone gives me some advise on this matter, I'd be grateful. |
Beta Was this translation helpful? Give feedback.
-
Since the grand goal, the quotient types, is yet out-of-reach, I thought that perhaps we may introduce something simpler...
Check out this little example.
What could go wrong?
What do you guys think about this?
Beta Was this translation helpful? Give feedback.
All reactions