Skip to content

Instantly share code, notes, and snippets.

Paolo G. Giarrusso Blaisorblade

Block or report user

Report or block Blaisorblade

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View ssreflect.v
Require Import ssreflect.
(*
Playing with
https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#type-families
*)
Lemma foo {a1 a2} : a1 = a2 -> a1 + a1 = a2 + a2.
Fail progress case.
(* Either one works, and gives a goal that can be dispatches by reflexivity. *)
@Blaisorblade
Blaisorblade / foo.agda
Created Jul 2, 2019
Level coercions in Agda
View foo.agda
module foo where
open import Data.Nat
open import Agda.Primitive
open import Level
foo = λ (T : (∀ (X : Set (lsuc lzero)) X X)) (X : Set lzero) T (Lift _ X)
View foo.agda
data _≡_ {i} {A : Set i} (x : A) : A -> Set i where
refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}
data Unit : Set where
unit : Unit
refl_unit : unit ≡ unit
refl_unit = refl
@Blaisorblade
Blaisorblade / sigT_cofe.v
Last active Jun 21, 2019
sigT forms an Iris Cofe, very different from sig
View sigT_cofe.v
From iris.algebra Require Import ofe.
Import EqNotations.
Unset Program Cases.
(* Subsumed by https://gitlab.mpi-sws.org/iris/stdpp/commit/4978faed45d1a1d84f79d3ec0456dd55d831b684 *)
Definition proj1_ex {P : Prop} {Q : P → Prop} (p : ∃ x, Q x) : P :=
let '(ex_intro _ x _) := p in x.
Definition proj2_ex {P : Prop} {Q : P → Prop} (p : ∃ x, Q x) : Q (proj1_ex p) :=
let '(ex_intro _ x H) := p in H.
View iris_proofmode_precedence.v
From iris.base_logic.lib Require Import invariants.
From iris.proofmode Require Import tactics.
Section foo.
Context `{Σ : gFunctors}.
Goal True ⊢ True : iProp Σ.
Proof.
iIntros.
(* Solves the goal, but needs the parens. *)
View CircularList.scala
object Init {
class Circular[A](val value: A, getter: => Circular[A]) {
lazy val get: Circular[A] = getter
}
def create[A](as: Traversable[A]): Circular[A] = {
def go[A](as: Traversable[A], initTail: => Circular[A]): Circular[A] = {
if (as.nonEmpty)
new Circular(as.head, go(as.tail, initTail))
else
View BugWithSingletonTypes.scala
object Test {
abstract class ExprBase { s =>
type A
}
abstract class Lit extends ExprBase { s =>
type A = Int
val n: A
}
@Blaisorblade
Blaisorblade / proof.v
Last active May 22, 2019
Limits of proof irrelevance on sigT — it's only legal when restricted, basically, to sig
View proof.v
Require Import Coq.ssr.ssreflect.
Require Import ProofIrrelevance.
Definition bad_sigma_irrelevance :=
(* Beware this P is in Type, not Prop; that's why this is inconsistent. *)
(* forall (U:Type) (P:U->Type) (x y:U) (p:P x) (q:P y), *)
(* equivalently: *)
forall (U:Type) P (x y: U) (p:P x) (q:P y),
x = y -> existT P x p = existT P y q.
View cofe_solver_produces_cofe.v
From iris.base_logic.lib Require Import iprop.
Section test.
Context `(Σ : gFunctors).
Import iProp_solution.
Import cofe_solver.
(* There is some duplication from https://gitlab.mpi-sws.org/iris/iris/blob/master/theories/base_logic/lib/iprop.v#L135-136. *)
(* That's needed here because iProp_result is hidden, so we re-define it. *)
Definition iProp_result :
solution (uPredCF (iResF Σ)) := solver.result (uPredCF (iResF Σ)).
View compile output.txt
$ ghc foo.hs
[1 of 1] Compiling Foo ( foo.hs, foo.o )
foo.hs:6:23: error:
• Couldn't match expected type ‘a’ with actual type ‘b’
‘b’ is a rigid type variable bound by
the type signature for:
notConst :: forall a b. a -> b -> a
at foo.hs:5:1-23
‘a’ is a rigid type variable bound by
You can’t perform that action at this time.