jespercockx

--{-# OPTIONS -v any-auto:10 #-}

open import Data.List
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.List.Relation.Unary.Any.Properties using
  (singleton⁺; map⁺; mapMaybe⁺; ++⁺ˡ; ++⁺ʳ; concat⁺)
open import Data.Maybe using (Maybe; nothing; just)
open import Data.Maybe.Relation.Unary.Any using (just) renaming (Any to MAny)
open import Data.Nat using (ℕ; zero; suc; _+_)

jespercockx

open import Data.List.Base

open import Data.Bool
open import Data.Empty
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_×_; _,_; uncurry)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
open import Data.Unit

jespercockx

open import Data.Bool.Base
open import Data.List.Base
open import Data.Nat.Base
open import Data.Product
open import Data.Unit

open import Function

open import Reflection
open import Reflection.TypeChecking.Monad.Syntax

jespercockx

-- This is an alternative solution to the problem discussed in the video https://www.youtube.com/watch?v=WplTbki3gCg

{-# LANGUAGE RankNTypes, StandaloneDeriving, DeriveAnyClass, TypeApplications, ScopedTypeVariables, GADTs #-}

import Data.Scientific
import Type.Reflection

data AnyRealFloat = AnyRealFloat (forall a. RealFloat a => a)

instance Eq AnyRealFloat where

jespercockx

/* Canonical Dedukti in LambdaPi

   An encoding of (my interpretation of) "Canonical Dedukti" by Thiago Felicissimo in LambdaPi

   All credit goes to Thiago, all blame goes to me
   -- Jesper, 2022-10-19
*/

/* syntactic classes */

jespercockx

open import Haskell.Prelude hiding (coerce; a; b; c; _,_; _,_,_)
open import Haskell.Extra.Erase
open import Haskell.Extra.Refinement
open import Scope
open import Utils

module STLC {@0 name : Set} where

private variable