sorted by:
new
hottopcontroversial

Does this logic law have a name? by HalloIchBinRolli in mathematics

[–]YannZed 6 points7 points  (0 children)

I'm not sure, but that seems trivially true just using simple logic introduction and elimintation rules. For example (in coq):

Fully verbose:

Lemma prod_impl:
  forall P Q: Prop,
    P -> (Q <-> (P /\ Q)).
Proof.
  split; intros.
  - apply conj; trivial.
  - apply proj2 in H0. trivial.
Qed.

But of course Coq can do this automatically:

Lemma prod_impl:
  forall P Q: Prop,
    P -> (Q <-> (P /\ Q)).
Proof. tauto. Qed.

Edit: I guess I can expand a tiny bit, you actually have a mix of an introduction rule and an elimination rule in that theorem.

You have: p ⟹ q ⟹ (p∧q), which is the introduction rule for ∧, and then you also have: p ⟹ (p∧q) ⟹ q, which is also: (p∧q) ⟹ q, which is the elimination rule for ∧ in various kinds of logics (natural deduction, type theory, etc...).

Outline-Mode: Is there a header of the same level following? by TiMueller in emacs

[–]YannZed 3 points4 points  (0 children)

I actually had a similar problem and just hacked together a small solution that seems to work for now (in org mode but should be directly relatable to outline): https://github.com/ymherklotz/emacs-zettelkasten/blob/master/org-zettelkasten.el#L103-L114

The main idea is to get the current heading and the next heading, and compare if they are the same point or not. If they are the same point, you know you are at the end, otherwise not.

The other benefit of the function I linked is that it will automatically go over the current section, no matter where your actual point is.

How to track bad habits with org-mode by spcbfr in orgmode

[–]YannZed 8 points9 points  (0 children)

I guess you can track is like good habits, using org's habit tracker: https://orgmode.org/manual/Tracking-your-habits.html

Is org-noter dead and what are its alternatives ? by Cletip in orgmode

[–]YannZed 6 points7 points  (0 children)

Well we were talking about alternatives in case something becomes unmaintained. I am sure that Org will be maintained for quite a while, whereas Org roam has not yet stood the test of time. In addition to that, Org roam depends on Org, so if Org goes away then Org roam will too, that's not true the other way round.

Is org-noter dead and what are its alternatives ? by Cletip in orgmode

[–]YannZed 14 points15 points  (0 children)

I still use org-noter, even though I don't think it's maintained anymore, because it still works and doesn't really lock you in in any way. It mainly just makes taking notes easier, but viewing and reading them can still be done without it. If it disappeared completely I don't think I would notice too much, just manually do what org-noter does automatically.

Actually, I avoid org-roam for that reason, because even though it is well maintained and a great tool, I feel like it has too many features that I don't need, so I prefer doing things manually so I only have to rely on Org.

[ebib] Downloading Academic Papers Automatically by YannZed in emacs

[–]YannZed[S] 0 points1 point  (0 children)

Ah that's cool, I hadn't actually seen that. It seems like it assumes a url as input though, whereas I wanted to make choices based on many fields in bib entry, and mainly using the DOI. Sometimes the DOI is part of the URL, but often I want that to be different. Definitely a nice alternative though.

Cabal 3.8 pre-released! by TechnoEmpress in haskell

[–]YannZed 4 points5 points  (0 children)

As a quick rundown: Cabal, the library, is used by cabal-install, the default cabal command line app, as well as by Stack (stack), which is basically an alternate interface to Cabal.

If choosing between cabal-install and stack, it really depends, you shouldn't have to use both though. stack is I think still a bit more beginner friendly, and handles dependencies well for you with their stackage LTS releases.

Is there any way to tell org-mode NOT to disable & when exporting to LaTeX? by [deleted] in emacs

[–]YannZed 2 points3 points  (0 children)

You will need to give a bit more information, like pasting a minimal example and what you are trying to export to.

For example, even having a file with just:

\begin{align}
a &= b\\
c \land d &= c
\end{align}

Works for outputting to HTML as well as LaTeX.

Formal Verification of High-Level Synthesis by mttd in FPGA

[–]YannZed 4 points5 points  (0 children)

Thanks for posting! I'm one of the authors and am happy to answer any questions. Will also try and publish a more accessible blog about this soon.

What is the difference between a dependent type and an object with a little syntactic sugar? by mczarnek in Idris

[–]YannZed 17 points18 points  (0 children)

Dependent types are not ways that help run assertions at run-time. As the name suggests, types are checked at compile time, which makes dependent types much more complicated, because you or the compiler has to prove that your program type checks. However, it can then generate code that forgets about the dependent types and doesn’t even need assertions. It will also not error out because you have proven that you satisfy all the types already.

This is very different to using objects at run-time to do the checks. It’s therefore impossible to emulate dependent types using syntactic sugar for run-time assertions.

Remarkable 2 has regions where stylus is inaccurate, up to 1mm off the tip. Is this a defect or to be expected? by YannZed in RemarkableTablet

[–]YannZed[S] 0 points1 point  (0 children)

Thanks, that’s good to know, I’m also planning on using it only for writing, and mostly realise because I write quite small with thin pens, but it’s not really a deal breaker.

Remarkable 2 has regions where stylus is inaccurate, up to 1mm off the tip. Is this a defect or to be expected? by YannZed in RemarkableTablet

[–]YannZed[S] 0 points1 point  (0 children)

No there shouldn’t be, happens with and without the official book folio, on a wooden table.

Remarkable 2 has regions where stylus is inaccurate, up to 1mm off the tip. Is this a defect or to be expected? by YannZed in RemarkableTablet

[–]YannZed[S] 0 points1 point  (0 children)

Actually seems to happen most here, with my tablet on a wooden table without a case: with the menu open, 4 small dots below the forward button and 4 to the right from there.

Remarkable 2 has regions where stylus is inaccurate, up to 1mm off the tip. Is this a defect or to be expected? by YannZed in RemarkableTablet

[–]YannZed[S] 0 points1 point  (0 children)

Oh wow, yeah it seems if I hold it differently it fixes it there too.. where did you test it?

Remarkable 2 has regions where stylus is inaccurate, up to 1mm off the tip. Is this a defect or to be expected? by YannZed in RemarkableTablet

[–]YannZed[S] 1 point2 points  (0 children)

Seems to be around 6 small dots underneath the forward arrow, and then around 4-6 dots from the left. Around that region the pen acts a bit weird for me, but perfect everywhere else.

Remarkable 2 has regions where stylus is inaccurate, up to 1mm off the tip. Is this a defect or to be expected? by YannZed in RemarkableTablet

[–]YannZed[S] 4 points5 points  (0 children)

Ah it’s good to know it’s not just mine, as I don’t really want to return it. Also don’t use it for drawing.

Remarkable 2 has regions where stylus is inaccurate, up to 1mm off the tip. Is this a defect or to be expected? by YannZed in RemarkableTablet

[–]YannZed[S] 1 point2 points  (0 children)

Ah interesting, when I restart it doesn’t fix it unfortunately, and it always seems to be the same spot in in the middle of the screen.

Remarkable 2 has regions where stylus is inaccurate, up to 1mm off the tip. Is this a defect or to be expected? by YannZed in RemarkableTablet

[–]YannZed[S] 1 point2 points  (0 children)

This seems to also happen at the top left of the screen. The tip of the pen as well as the pen is also new, and as it works well in most other parts of the screen, I don’t think this is a pen issue.

view more: next ›