TOTBWF

module 1Lab.Reflection.Duh where

open import 1Lab.Reflection
open import 1Lab.Prelude
open import Data.List
open import Data.Nat

private
  try-all : Term → Nat → Telescope → TC Term
  try-all goal _ [] = typeError $ strErr "Couldn't find anything!" ∷ []

andrejbauer

{- Here is a short demonstration on how to use Agda's solvers that automatically
   prove equations. It seems quite impossible to find complete worked examples
   of how Agda solvers are used.

   Thanks go to @anormalform who helped out with these on Twitter, see
   https://twitter.com/andrejbauer/status/1549693506922364929?s=20&t=7cb1TbB2cspIgktKXU8rng

   I welcome improvements and additions to this file.

   This file works with Agda 2.6.2.2 and standard-library-1.7.1

xpqz

⎕USING←'System.Collections'
openWith←⎕NEW Hashtable
⍝ Add some elements to the hash table. There are no
⍝ duplicate keys, but some of the values are duplicates.
openWith.Add'txt' 'notepad.exe'
openWith.Add'bmp' 'paint.exe'
openWith.Add'dib' 'paint.exe'
openWith.Add'rtf' 'wordpad.exe'
openWith
(⌷openWith).(Key Value)

larrytheliquid

There are a lot of resources to learn from, and it's hard to pick just one. Below are links to learning about dependently typed programming. I think that the most comfortable path is to learn DT programming first, and then learn more of the pure math and type theory behind it along the way as you get more experienced.

Basically, Coq is the most mature and oldest, but is more tedious to do dependently typed programming with.
Agda is not as mature, but it supports dependently typed programming very well.
Idris is an even newer language that also supports dependently typed programming well, and IMO has the best chance of being a practically used language.
Personally, I mostly use Agda.

Coq:
Software foundations - http://www.cis.upenn.edu/~bcpierce/sf/toc.html
Certified programming with dependent types - http://adam.chlipala.net/cpdt/

phadej

module SystemF where

open import Agda.Primitive
open import Prelude
open import Data.List

weaken-∈ : ∀ {a : Set} (Γ₁ : List a) {Γ x y} → x ∈ (Γ₁ ++ Γ) → x ∈ (Γ₁ ++ y ∷ Γ)
weaken-∈ [] (zero refl) = suc (zero refl)
weaken-∈ [] (suc i) = suc (suc i)
weaken-∈ (x ∷ Γ₁) (zero p) = zero p

aztek

open import Level using (_⊔_)
open import Function
open import Data.Fin using (Fin; zero; suc)
open import Data.Nat hiding (_⊔_)
open import Data.Nat.Properties
open import Data.Vec
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Core

LeoAdamek

acks :: [[Int]]
acks = [ [ case (m, n) of
                (0, _) -> n + 1
                (_, 0) -> acks !! (m - 1) !! 1
                (_, _) -> acks !! (m - 1) !! (acks !! m !! (n - 1))
         | n <- [0..] ]
       | m <- [0..] ]

main :: IO ()
main = print $ acks !! 4 !! 1

andrejbauer

(* How do to topology in Coq if you are secretly an HOL fan.
   We will not use type classes or canonical structures because they
   count as "advanced" technology. But we will use notations.
 *)

(* We think of subsets as propositional functions.
   Thus, if [A] is a type [x : A] and [U] is a subset of [A],
   [U x] means "[x] is an element of [U]".
*)
Definition P (A : Type) := A -> Prop.