Skip to content
Snippets Groups Projects
Commit b4f44c90 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Coqdoc.

parent 21de4a02
Branches
Tags
No related merge requests found
......@@ -3,7 +3,7 @@ From stdpp Require Export list numbers list_numbers fin.
From stdpp Require Import options.
Local Open Scope positive.
(* Note that [Countable A] gives rise to [EqDecision A] by checking equality of
(** Note that [Countable A] gives rise to [EqDecision A] by checking equality of
the results of [encode]. This instance of [EqDecision A] is very inefficient, so
the native decider is typically preferred for actual computation. To avoid
overlapping instances, we include [EqDecision A] explicitly as a parameter of
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment