michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Decidables: adds a word fix to a version under extra

Browse source
This commit is contained in:
Marko Dimjašević 2019-01-24 21:07:03 +01:00 committed by Wen Kokke
parent 3ef2ee4bed
commit 6ec9eea5c8
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
extra/extra/DecidableExtra.lagda
View file

@ -193,7 +193,7 @@ The forward proof has one more clause than the reverse proof,
precisely because in the forward proof we need clauses corresponding to precisely because in the forward proof we need clauses corresponding to
the comparison yielding both true and false, while in the reverse proof the comparison yielding both true and false, while in the reverse proof
we only need clauses corresponding to the case where there is evidence we only need clauses corresponding to the case where there is evidence
that the comparision holds. This is exactly why we tend to prefer the that the comparison holds. This is exactly why we tend to prefer the
evidence formulation to the computation formulation, because it allows evidence formulation to the computation formulation, because it allows
us to do less work: we consider only cases where the relation holds, us to do less work: we consider only cases where the relation holds,
and can ignore those where it does not. and can ignore those where it does not.