For this presentation, we keep the dependencies to a minimum.
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 |
/* 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 */ |
-- 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 |
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 |
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 |
--{-# 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; _+_) |
{-# OPTIONS --rewriting #-} | |
open import Data.Empty using (⊥; ⊥-elim) | |
open import Data.Unit using (⊤; tt) | |
open import Data.Bool using (Bool; true; false; if_then_else_) | |
open import Data.Product using (Σ; Σ-syntax; _×_; _,_; proj₁; proj₂) | |
open import Relation.Binary.PropositionalEquality | |
Π : (A : Set) (B : A → Set) → Set | |
Π A B = (x : A) → B x |
open import Agda.Primitive | |
open import Data.Bool.Base | |
open import Data.Nat.Base | |
open import Data.List.Base | |
open import Data.Product using (_×_; _,_; proj₁; proj₂) | |
import Data.String.Base as String | |
open import Data.Unit.Base | |
open import Function using (id; _∘_) |
{-# OPTIONS --without-K #-} | |
open import Agda.Builtin.Equality | |
_∘_ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} | |
→ (f : {x : A} (y : B x) → C y) (g : (x : A) → B x) | |
→ (x : A) → C (g x) | |
(f ∘ g) x = f (g x) | |
_⁻¹ : {A : Set} {x y : A} → x ≡ y → y ≡ x |