Patrick Nicodemus
Patrick Nicodemus
TL; DR - I would like the GW function to provide an option to skip the line search in favor of the naive update step, because in my experiments line...
Currently several algorithms to compute or estimate Gromov-Wasserstein distance are provided, so the user has lots of freedom to experiment with algorithms which are appropriate to their particular distribution size,...
I have the following anomaly: ``` From Coq Require Import StrictProp. From Hammer Require Import Tactics Hammer. Fixpoint s_eq_nat (n m : nat): SProp := match n with | O...
Ltac2 currently does not appear to know about the Coq typeclass system. ```coq From Ltac2 Require Import Ltac2. Class myclass (A : Type) := { a : A }. Instance...
The documentation on modules is incomplete. https://agda.readthedocs.io/en/v2.6.4.1/language/module-system.html It should be edited so that "Module application" and "Anonymous modules" are nonempty. @plt-amy As the 1lab makes frequent use of anonymous modules,...
# Description Let $F: C\times D\to B$ be a functor and $p : E\to B$ a displayed category. Let $F' : C\times D\to E$ be a lift of $F$ along...
I am curious what would have to be done in order to get this software compatible with Ocaml 5. How serious of an undertaking would this be? What are the...
As of version 3.3, Sphinx provides the functionality for a dictionary called `autodoc_type_aliases` in which the user can explicitly put type aliases that they do not want the autodoc to...
When I open Emacs and run the command `opam config exec -- dune utop . -- -emacs`, it creates a new buffer which is blank and does not accept text...
I have started trying to use owl for a project to identify good avenues for improvement. Two issues I came across when I tried using dataframes: - Option types are...