Commit e59779e5 authored by Nicola Botta's avatar Nicola Botta
Browse files

Initial.

parent 884df118
> module Pairs.Operations
> import Sigma.Sigma
> %default total
> %access public export
> %auto_implicits on
> -- %hide getWitness
> -- %hide getProof
> {-
> namespace Exists
> getWitness : {P : a -> Type} -> Exists {a} P -> a
> getWitness (Evidence x pf) = x
> getProof : {P : a -> Type} -> (x : Exists {a} P) -> P (getWitness x)
> getProof (Evidence x pf) = pf
> namespace Subset
> getWitness : {P : a -> Type} -> Subset a P -> a
> getWitness (Element x pf) = x
> getProof : {P : a -> Type} -> (x : Subset a P) -> P (getWitness x)
> getProof (Element x pf) = pf
> ---}
> namespace Sigma
> getWitness : {P : a -> Type} -> Sigma a P -> a
> getWitness (MkSigma x pf) = x
> getProof : {P : a -> Type} -> (x : Sigma a P) -> P (getWitness x)
> getProof (MkSigma x pf) = pf
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment