Skip to content

Instantly share code, notes, and snippets.

View peterbb's full-sized avatar

Peter Brottveit Bock peterbb

View GitHub Profile
{-# OPTIONS_GHC -XViewPatterns #-}
module Derivation
where
import Control.Monad.Error
-- import AbstractTree
-- Stump definition of Expr
data Expr = Variable String Int | Type | Kind deriving (Eq)
@peterbb
peterbb / gist:6892368
Created October 8, 2013 21:47
Using the tactic "dependent induction" inside a match goal seems not to work.
subtype_weaken_l < Show.
1 subgoal
C : constraints
AT : annotatedtype
AT' : annotatedtype
H : subtype C AT AT'
============================
forall C' : list ineq, subtype (C ++ C') AT AT'
Section TMP.
Variable A : Set.
Variables a b : A.
Definition f (n : nat) : A :=
match n with
| 0 => a
| _ => b
end.
record Snapshot Θ a : Set where
constructor snapshot
field
{Δ} : StackType
stack : Stack Δ
{Γ} : Cxt
environment : Env Γ
control : Control Γ (Θ ++ Δ) (a ∷ [])
Require Import ZArith FMapPositive.
Open Scope positive.
(* -------- Works, but does not keep variables apart ------ *)
Definition const_t : Set := positive.
Definition var_t : Set := positive.
Opaque const_t var_t.
Inductive ex1 : Set :=
| ex1_const : const_t -> ex1
Module Type GAxioms.
Axiom U : Set.
Axiom causes : U -> U -> Prop.
Axiom isPartOf : U -> U -> Prop.
Definition S (r : U) : Prop := causes r r.
Definition C (r : U) : Prop := exists s, causes r s.
Definition O (q : U) : Prop := forall t, causes q t.
Axiom A1 : forall r, exists v, causes v r.
Module Type OpaqueSomething.
Parameter T : Type.
Parameter t : T.
End OpaqueSomething.
Module OpaqueNat : OpaqueSomething with Definition T := nat.
Definition T := nat.
Definition t := 0.
End OpaqueNat.
@peterbb
peterbb / Example.kt
Last active February 15, 2022 10:13
Named, typed parameters for java.sql.PreparedStatement in Kotlin
object GetUser: Template() {
var id by SqlInt
var name by SqlString
override fun query() = """
(select * from users where name = $name and id = $id)
union
(select * from deleted_user where id = $id)
"""
}