Skip to content

Instantly share code, notes, and snippets.

@ybertot

ybertot/using hiearchy-builder mathcomp

Created April 16, 2021 08:13
Show Gist options
  • Save ybertot/9c72c7c25afdc9d3f2fdd668f3313c4d to your computer and use it in GitHub Desktop.
Save ybertot/9c72c7c25afdc9d3f2fdd668f3313c4d to your computer and use it in GitHub Desktop.
Download ZIP
Example of using EqMixin and siblings to create eqtypes
Raw
using hiearchy-builder mathcomp
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
Inductive i3 := c1 | c2 | c3.
Definition i3dec (x y : i3) : {x = y}+{x <> y}.
move: x y=> [ | | ][ | | ]; (by (left)) || (by right).
Defined.
Fail Lemma toto : c1 == c1.
HB.instance Definition _ := HasDecEq.Build i3 (compareP i3dec).
Lemma toto (x : i3) : x == x.
Proof. by []. Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment