UlfNorell

-- Challenge: https://github.com/effectfully/random-stuff/blob/master/RecN-challenge.agda
{-# OPTIONS --type-in-type #-}  -- Just for convenience, not essential.

open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Base

coerce : ∀ {A B} -> A ≡ B -> A -> B
coerce refl = id

UlfNorell

open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.String
open import Agda.Builtin.IO
open import Agda.Builtin.Unit

{-# FOREIGN GHC
import Data.Text
import qualified Data.Text.IO as Text

UlfNorell

{-# OPTIONS --rewriting #-}

module _ where

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Unit
open import Agda.Builtin.String renaming (primStringEquality to _==_)
open import Agda.Builtin.List

UlfNorell

-- Reversing an ascending list in Agda.
-- Challenge by @arntzenius: https://twitter.com/arntzenius/status/1034919539467677696
module AscList where

-- We'll go without libraries to make things clearer.

flip : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → (A → B → C) → B → A → C
flip f x y = f y x

-- Step one is to define ordered lists. We'll roughly follow Conor McBride's approach

UlfNorell

-- Problem 3 of @Hillelogram's Great Theorem Prover Showdown.
-- https://www.hillelwayne.com/post/theorem-prover-showdown
--
-- Implemented using current stable-2.5 branch of Agda
-- (https://github.com/agda/agda/tree/08664ac) and the agda-prelude
-- library (https://github.com/UlfNorell/agda-prelude/tree/d193a94).

module Fulcrum where

open import Prelude hiding (_≤?_)

UlfNorell

-- In response to https://lists.chalmers.se/pipermail/agda/2017/009872.html
module _ where

open import Agda.Builtin.Equality

infix 0 case_of_
case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

-- Equality reasoning --

UlfNorell

module _ where

open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Nat hiding (_<_; _≤_) renaming (_<′_ to _<_; _≤′_ to _≤_)
open import Data.Nat.Properties
open import Data.Nat.Properties.Simple
open import Data.Product
open import Data.Empty

UlfNorell

open import Prelude
open import Builtin.Reflection
open import Tactic.Reflection.Quote

data TTerm {a} (A : Set a) : Set where
  typed : Term → TTerm A

mkTyped : ∀ {a} {A : Set a} → A → Term → TTerm A
mkTyped _ t = typed t