Blaisorblade

Require Import List.
Import ListNotations.

Inductive ForallT {A : Type} (P : A -> Type) : list A -> Type :=
| ForallT_nil : ForallT P []
| ForallT_cons (x : A) (l : list A) : P x -> ForallT P l -> ForallT P (x :: l).
Hint Constructors ForallT : core.

Definition fold_ForallT {A R : Type} {P: A -> Type}
    (hnil : R) (hcons : forall (a : A), P a -> R -> R)

Blaisorblade

Coq Language Server: process.version: v10.11.0, process.arch: x64}
Loaded project at /Users/pgiarrusso/git/Coq/dot-iris
Changed path to: /Users/pgiarrusso/.opam/coq-8.8.2/bin/
starting coqtop
exec: /Users/pgiarrusso/.opam/coq-8.8.2/bin/coqtop -v
Listening at 127.0.0.1:50060
Listening at 127.0.0.1:50061
Listening at 127.0.0.1:50062
Listening at 127.0.0.1:50063
Detected coqtop version 8.8.2

Blaisorblade

$ brew cask upgrade --verbose --debug
==> Casks with `auto_updates` or `version :latest` will not be upgraded
==> Upgrading 1 outdated package:
intel-power-gadget 3.5.5,828382 -> 3.6.1,833853
==> Started upgrade process for Cask intel-power-gadget
==> Upgrading intel-power-gadget
==> Printing caveats
==> Printing caveats
==> Caveats
To install and/or use intel-power-gadget you may need to enable its kernel extension in:

Blaisorblade

Require Import Omega.

Lemma foo (n n0 n1 n2 n3 n4: nat):
n + (n0 + n1) = 0 ->
n2 + (n3 + n4) = 0 ->
n0 + n3 + n + n2 + (n1 + n4) = 0.
Proof. omega. Qed.

Blaisorblade

Require Coq.Vectors.Vector.

Definition splitVec {A n} (xs : Vector.t A (S n)): A * Vector.t A n :=
  match xs with
  (* | Vector.nil _ => _ (* fun A (a: A) => a *) *)
  | Vector.cons _ x n0 xs => (x, xs)
  end.

(* Alternative version. *)
Definition splitVec2 {A n} (xs : Vector.t A (S n)): A * Vector.t A n.

Blaisorblade

Notation "⊤" := True : dms_scope.
Notation " {@ T1 } " := ( and T1 True ) (format "{@  T1  }"): dms_scope.
Notation " {@ T1 ; T2 ; .. ; Tn } " :=
  (and T1 (and T2 .. (and Tn True)..))
  (format "'[v' {@  '[' T1 ']'  ;  '//' '[' T2 ']'  ;  '//' ..  ;  '//' '[' Tn ']'  } ']'") : dms_scope.
Open Scope dms_scope.
Close Scope dms_scope.
Delimit Scope dms_scope with dms.
Check {@ True ; True -> False ; False } % dms.

Blaisorblade

Notation "⊤" := True : dms_scope.
Notation " {@ T1 } " := ( and T1 True ) (format "{@  T1  }"): dms_scope.
Notation " {@ T1 ; T2 ; .. ; Tn } " :=
  (and T1 (and T2 .. (and Tn True)..))
  (* (format "'[v' {@  '[' T1 ']'  ;  '//' T2  ;  '//' ..  ;  '//' Tn  } ']'") *)
   : dms_scope.
Open Scope dms_scope.
Close Scope dms_scope.
Delimit Scope dms_scope with dms.

Blaisorblade

module CyclicFin where

open import Agda.Builtin.Equality
open import Agda.Builtin.TrustMe
open import Agda.Builtin.Nat
open import Data.Nat
  renaming ( _+_ to _+ℕ_ ; _^_ to _^ℕ_ ; _<_ to _<ℕ_ )
import Data.Nat.Properties as NatProp
open import Data.Nat.DivMod

Blaisorblade

module DoesNotTypecheck-Unexpected where
  -- ... up to addableℚ

  -- Use this where _+_ triggers yellow highlighting.
  _+'_ = _+_ {{addableℚ}}

  ◁-ineq : ∀ a b c → ∣ a - c ∣ ≤ ∣ a - b ∣ + ∣ b - c ∣
  ◁-ineq a b c =              begin
    ∣ a - c ∣                 ≡⟨ cong (λ x → ∣ a +' x  ∣) (sym (+-identityˡ (- c))) ⟩
                                                -----

Blaisorblade

open import Data.Fin
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Sum
open import Relation.Binary.PropositionalEquality

even : ℕ → Set
even n = (n mod 2) ≡ 0F

odd : ℕ → Set