## Where communities thrive

• Join over 1.5M+ people
• Join over 100K+ communities
• Free without limits
##### Activity
• Jul 13 2021 11:54

dependabot[bot] on bundler

• Jul 13 2021 11:53

Bump addressable from 2.5.2 to … Merge pull request #285 from si… (compare)

• Jul 13 2021 11:53
• Jul 13 2021 01:13
dependabot[bot] labeled #285
• Jul 13 2021 01:13
dependabot[bot] opened #285
• Jul 13 2021 01:13

dependabot[bot] on bundler

Bump addressable from 2.5.2 to … (compare)

• Jul 13 2021 01:12

dependabot[bot] on bundler

• Jul 13 2021 01:12

Bump addressable from 2.5.2 to … Merge pull request #284 from si… (compare)

• Jul 13 2021 01:12
• Jul 13 2021 01:03
dependabot[bot] labeled #284
• Jul 13 2021 01:03
dependabot[bot] opened #284
• Jul 13 2021 01:03

dependabot[bot] on bundler

Bump addressable from 2.5.2 to … (compare)

• Mar 01 2020 03:32

dependabot[bot] on bundler

• Mar 01 2020 03:32

Bump rake from 12.0.0 to 12.3.3… Merge pull request #283 from si… (compare)

• Mar 01 2020 03:32
• Mar 01 2020 01:50
dependabot[bot] labeled #283
• Mar 01 2020 01:50
dependabot[bot] opened #283
• Mar 01 2020 01:50

dependabot[bot] on bundler

Bump rake from 12.0.0 to 12.3.3… (compare)

• Mar 01 2020 01:50

dependabot[bot] on bundler

• Mar 01 2020 01:50

Bump rake from 12.0.0 to 12.3.3… Merge pull request #282 from si… (compare)

How do you write a type that shows that an implication implies its contrapositive? The type of such a thing looks like this, I suppose : impliesContrapositive : (A : Type) -> (B : Type) -> (A -> B) -> ((B -> Void) -> (A -> Void))
Is such a thing possible to write, or is it preferable to do a different thing to achieve the same result?
The law of excluded middle is not normally part of the foundations, and is needed for contrapositive being equivalent to the statement. The reason we don't have it is that it does not give a concrete value, and we want concrete values.
By the law of excluded middle for the type $A$ is $A \oplus (A \to Void)$
$A \oplus (A \to 0)$
Here, I meant the 0 type , so should have said
$lem(A) = A \oplus (A \to \mathbb{0}$
Sorry,
lem(A)= A \oplus (A \to \mathbb{0})
$lem(A)= A \oplus (A \to \mathbb{0})$
The contrapositive in the form you said it is true though,
$(A \to B) \to (B \to 0) \to (A \to 0)$
This can be proved, i.e., we get a term
$(f : A \to B) \mapsto (c : B \to \mathbb{0}) \mapsto a : A \mapsto c(f(a))$
bnag098
@bnag098

I am having some trouble in using the replace function.
I was trying to substitute $0$ using the equality $0 = b \cdot 0$ in $c = 0 + c$ to hopefully get $c = b \cdot 0 + c$.
But in the function call below:

replace (sym (multZeroRightZero b)) (sym (plusZeroLeftNeutral c))

I am getting an error claiming that in the second variable of replace, idris expects a value of the type P 0. The documentation on this P function couldn't explain much. Any help here would be appreciated.

SS-C4
@SS-C4
Is it possible to case split on a dependent pair?
For example, if I want to use the pair (x **pf) in a function, where I want to case split on x being Z or (S k), and I need the proof when this happens.
case (fst (x**pf)) of typechecks, but the proof type does not change, and stays the same as the original.
SS-C4
@SS-C4
Oh, I found it. with helps here.
To capture the notion of a total order, in which exactly one of three things can occur, a<=b and !(a>=b), !(a<=b) and (a>=b) or (a<=b) and (a>=b), would the best thing to do be to define a new type along the lines of Either, or would it be better to try to work with existing types to get something with the same behaviour?
Generally best to define a new type, though this one may be in the standard library or contrib (look for trichotomy).
Using combinations of pairs, dependent pairs and coproducts (Either) makes stuff hard to understand, parse by idris and also more error-prone (a wrong type may be accepted because of the same structure).
Would it be preferable to define the order on the naturals as arising from addition rather than the inductive one defined in the standard library?
Yes, it may work better. In any case if you prove the two are equivalent,
you can use both definitions
shafilmaheenn
@shafilmaheenn
Is there a way to check whether 2 functions have the same name in the entire code folder?
Atom has a search in folder, ctrl-shift-f, which can also be filtered, here using *.idr for filename
shafilmaheenn
@shafilmaheenn
As a lot of theorems about gcd need the bezout's lemma, may I use assert_total in the bez and GCDCalc function which essentially follow Euclid's algorithm?. I have no clue on how to convince idris that Euclid's algorithm is total without that.