rybla

Keybase proof

I hereby claim:

• I am riib11 on github.
• I am riib11 (https://keybase.io/riib11) on keybase.
• I have a public key ASBdNRCAVuixD-Vp9Y0D3GqiVHQtw44UV-t2tMRAu1BHtwo

To claim this, I am signing this object:

rybla

open import Level
open import Relation.Binary


module AlgebraicFieldExtension {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (α : A) where


open import Function
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

rybla

module StructureField where


open import Level using (_⊔_; suc)
open import Relation.Binary using (Rel)
open import Relation.Nullary using (¬_)

open import Algebra.Core
open import Algebra.Structures as Structures

rybla

open import Function
open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropositionalEquality
open import Relation.Nullary
open import Algebra

-- based on Zalakain's "Evidence-Providing Problem Solvers in Agda"
-- href: https://umazalakain.info/static/report.pdf

rybla

module ListFailure where


import           Prelude                 hiding ( head
                                                , tail
                                                )


{-@
data List a = Nil | Cons { head :: a , tail :: List a }

rybla

module LMonadEquality where

import LFunctor -- Liquid Haskell Functor data class

--------------------------------------------------------------------------------
-- Monad
--------------------------------------------------------------------------------

-- Data Class.
{-@

rybla

{-
# Relation
-}

{-@
type Re r a RE X Y = {_:r a | RE X Y}
@-}

{-@
newtype IsReflexive r a <re :: a -> a -> Bool> = IsReflexive

rybla

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module InaccessiblePattern where

rybla

module Inductive where

open import Data.Empty
open import Data.Unit
open import Data.Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.Product
open import Data.Sum

module Inductive

rybla

{-# LANGUAGE GADTs, KindSignatures, DataKinds, RankNTypes, TypeFamilies, TypeFamilyDependencies, AllowAmbiguousTypes, ScopedTypeVariables #-}

module OverloadSingletonI where

import Prelude hiding (negate)

data OverloadMode = NegateInt | NegateBool 

data SOverloadMode :: OverloadMode -> * -> * where
  SNegateInt :: SOverloadMode NegateInt (Int -> Int)