co-dan

diff --git a/theories/list.v b/theories/list.v
index 2f1db8e..a200405 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2988,6 +2988,11 @@ Section setoid.
   Proof. induction n; destruct 1; simpl; try constructor; auto. Qed.
   Global Instance list_lookup_proper i : Proper ((≡@{list A}) ==> (≡)) (lookup i).
   Proof. induction i; destruct 1; simpl; try constructor; auto. Qed.
+  Global Instance list_lookup_total_proper `{!Inhabited A} i :
+    Proper ((≡@{list A}) ==> (≡)) (lookup_total i).

co-dan

Fixpoint code_poly (P Q : polynomial) : Type := 
  match P, Q with
  | poly_var, poly_var => Unit
  | poly_const C, poly_const C' => C = C'
  | poly_times Q R, poly_times Q' R' => (code_poly Q Q') * (code_poly R R')
  | poly_plus Q R , poly_plus Q' R'  => (code_poly Q Q') * (code_poly R R')
  | _, _ => Empty
  end.

co-dan

module Map2 where

--------------------------------------------------
-- * Prelude
--------------------------------------------------
-- Taken from: https://github.com/pigworker/Ohrid-Agda
open import Ohrid-Prelude
open import Ohrid-Nat

-- Mini HoTT (Except that we have K)

co-dan

(** Well-founded relations in intuitionistic type theory *)
(** last updated : 5 of April, 2017. email: dfrumin [at] cs.ru.nl *)
Definition relation A := A -> A -> Prop.

Section wf.
  Variable A : Type.
  Variable R : relation A.
  Notation "x '<' y" := (R x y).

  (** * Intuitionistic well-foundedness criteria *)

co-dan

let x = ref (fun z -> z) in
let f = fun z -> (!x) z in
x := f; f ()

(* f () → (!x) () → f () → ... *)

co-dan

#lang racket
(require racket/dict) ;; for dict-lookup for env

; eval-apply interpreter for call-by-value λ-calculus with call/cc
; scroll down to test1, test2 and yin & yang to see example programs

(define id (lambda (x) x))
(define initev '())
(define (ext k v e) 
  (cons (cons k v) e))

co-dan

{-# LANGUAGE OverloadedStrings #-}
import           Control.Monad
import           Control.Monad.Identity
import           Control.Monad.Random
import qualified Data.ByteString                        as BS
import qualified Data.ByteString.Char8                  as B
import           Data.Maybe
import           Data.Set                               as S
import           Data.Traversable                       as T
import           Pipes

co-dan

Require Import Rel.
Require Import Coq.Init.Wf.

Theorem nat_wo: well_founded lt.
Proof.
  intro n.
  assert (forall y x, x < y -> Acc lt x) as A.
  induction y.
  + intros x H; inversion H.
  + intros x H'. apply Acc_intro.

co-dan

Inductive gorgeous : nat -> Prop :=
  g_0 : gorgeous 0
| g_plus3 : forall n, gorgeous n -> gorgeous (3+n)
| g_plus5 : forall n, gorgeous n -> gorgeous (5+n).
Fixpoint gorgeous_ind_max (P: forall n, gorgeous n -> Prop) (f : P 0 g_0)
         (f0 : forall (m : nat) (e : gorgeous m), 
               P m e -> P (3+m) (g_plus3 m e)) 
         (f1 : forall (m : nat) (e : gorgeous m), 
               P m e -> P (5+m) (g_plus5 m e)) 
         (n : nat) (e: gorgeous n) : P n e :=

co-dan

{-# LANGUAGE OverloadedStrings #-}

module Controllers.Home (homeRoutes) where

import Web.Scotty
import Data.Monoid                              (mconcat)
import qualified Database.RethinkDB as R
import qualified Database.RethinkDB.NoClash

homeRoutes :: ScottyM ()