Add example

Author: kazk

bin/run

@@ -0,0 +1,14 @@
+#!/bin/env bash
+set -eu
+
+W=/workspace/agda
+# Create container
+C=$(docker container create --rm -w $W ghcr.io/codewars/agda:latest agda --verbose=0 --include-path=. --library=standard-library --library=cubical ExampleTest.agda)
+
+# Copy files from the current directory
+# example/Example.agda
+# example/ExampleTest.agda
+docker container cp example/. $C:$W
+
+# Run tests
+docker container start --attach $C

example/Example.agda

@@ -0,0 +1,6 @@
+{-# OPTIONS --safe #-}
+module Example where
+open import Agda.Builtin.Equality
+
+_⇆_ : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
+refl ⇆ refl = refl

example/ExampleTest.agda

@@ -0,0 +1,7 @@
+{-# OPTIONS --safe #-}
+module ExampleTest where
+open import Agda.Builtin.Equality
+open import Example
+
+check : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
+check = _⇆_