peterbb

{-# 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

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'

peterbb

Section TMP.
    Variable A : Set.
    Variables a b : A.

    Definition f (n : nat) : A :=
        match n with
        | 0 => a
        | _ => b
        end.

peterbb

record Snapshot Θ a : Set where
  constructor snapshot
  field
    {Δ}         : StackType
    stack       : Stack Δ
    {Γ}         : Cxt
    environment : Env Γ
    control     : Control Γ (Θ ++ Δ) (a ∷ [])

peterbb

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

peterbb

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.

peterbb

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

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)
    """
}