blob: 9d86c08d71f37a9b456b4e3a800bb2bee39020c9 (
plain)
1
2
3
4
5
6
7
8
|
From Coq Require Import Cyclic31.
Definition Nat `(int31) := nat.
Definition Zero (_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _: digits) := 0.
Check (eq_refl (int31_rect Nat Zero 1) : 0 = 0).
Check (eq_refl (int31_rect Nat Zero 1) <: 0 = 0).
Check (eq_refl (int31_rect Nat Zero 1) <<: 0 = 0).
|
