Idrall.Expr

Reexports

import public Idrall.FC
import public Data.SortedMap

Definitions

Name : Type

Visibility: public export

data FieldName : Type

Totality: total
Visibility: public export
Constructor:

MkFieldName : String -> FieldName

Hints:

Eq FieldName
Ord FieldName
Show FieldName

prettyFieldName : FieldName -> String

Visibility: public export

Namespace : Type

Visibility: public export

data U : Type

Totality: total
Visibility: public export
Constructors:

CType : U
Sort : U
Kind : U

Hints:

Eq U
Show U

data ImportStatement : Type

Totality: total
Visibility: public export
Constructors:

LocalFile : FilePath -> ImportStatement
EnvVar : String -> ImportStatement
Http : String -> ImportStatement
Missing : ImportStatement

Hints:

Show ImportStatement
Show (Import ImportStatement)

data Import : Type -> Type

Totality: total
Visibility: public export
Constructors:

Raw : a -> Import a
Text : a -> Import a
Location : a -> Import a
Resolved : Expr Void -> Import a

Hints:

Show (Import ImportStatement)
Show (Import a)

data Chunks : Type -> Type

Totality: total
Visibility: public export
Constructor:

MkChunks : List (String, Expr a) -> String -> Chunks a

Hints:

Monoid (Chunks a)
Semigroup (Chunks a)
Show (Chunks a)

data Expr : Type -> Type

Totality: total
Visibility: public export
Constructors:

EConst : FC -> U -> Expr a
EVar : FC -> Name -> Int -> Expr a
ELam : FC -> Name -> Expr a -> Expr a -> Expr a
EPi : FC -> Name -> Expr a -> Expr a -> Expr a
EApp : FC -> Expr a -> Expr a -> Expr a
ELet : FC -> Name -> Maybe (Expr a) -> Expr a -> Expr a -> Expr a
EAnnot : FC -> Expr a -> Expr a -> Expr a
EBool : FC -> Expr a
EBoolLit : FC -> Bool -> Expr a
EBoolAnd : FC -> Expr a -> Expr a -> Expr a
EBoolOr : FC -> Expr a -> Expr a -> Expr a
EBoolEQ : FC -> Expr a -> Expr a -> Expr a
EBoolNE : FC -> Expr a -> Expr a -> Expr a
EBoolIf : FC -> Expr a -> Expr a -> Expr a -> Expr a
ENatural : FC -> Expr a
ENaturalLit : FC -> Nat -> Expr a
ENaturalFold : FC -> Expr a
ENaturalBuild : FC -> Expr a
ENaturalIsZero : FC -> Expr a
ENaturalEven : FC -> Expr a
ENaturalOdd : FC -> Expr a
ENaturalToInteger : FC -> Expr a
ENaturalSubtract : FC -> Expr a
ENaturalShow : FC -> Expr a
ENaturalPlus : FC -> Expr a -> Expr a -> Expr a
ENaturalTimes : FC -> Expr a -> Expr a -> Expr a
EInteger : FC -> Expr a
EIntegerLit : FC -> Integer -> Expr a
EIntegerShow : FC -> Expr a
EIntegerClamp : FC -> Expr a
EIntegerNegate : FC -> Expr a
EIntegerToDouble : FC -> Expr a
EDouble : FC -> Expr a
EDoubleLit : FC -> Double -> Expr a
EDoubleShow : FC -> Expr a
EText : FC -> Expr a
ETextLit : FC -> Chunks a -> Expr a
ETextAppend : FC -> Expr a -> Expr a -> Expr a
ETextShow : FC -> Expr a
ETextReplace : FC -> Expr a
EList : FC -> Expr a
EListLit : FC -> Maybe (Expr a) -> List (Expr a) -> Expr a
EListAppend : FC -> Expr a -> Expr a -> Expr a
EListBuild : FC -> Expr a
EListFold : FC -> Expr a
EListLength : FC -> Expr a
EListHead : FC -> Expr a
EListLast : FC -> Expr a
EListIndexed : FC -> Expr a
EListReverse : FC -> Expr a
EOptional : FC -> Expr a
ESome : FC -> Expr a -> Expr a
ENone : FC -> Expr a
EEquivalent : FC -> Expr a -> Expr a -> Expr a
EAssert : FC -> Expr a -> Expr a
ERecord : FC -> SortedMap FieldName (Expr a) -> Expr a
ERecordLit : FC -> SortedMap FieldName (Expr a) -> Expr a
EUnion : FC -> SortedMap FieldName (Maybe (Expr a)) -> Expr a
ECombine : FC -> Expr a -> Expr a -> Expr a
ECombineTypes : FC -> Expr a -> Expr a -> Expr a
EPrefer : FC -> Expr a -> Expr a -> Expr a
ERecordCompletion : FC -> Expr a -> Expr a -> Expr a
EMerge : FC -> Expr a -> Expr a -> Maybe (Expr a) -> Expr a
EToMap : FC -> Expr a -> Maybe (Expr a) -> Expr a
EField : FC -> Expr a -> FieldName -> Expr a
EProject : FC -> Expr a -> Either (List FieldName) (Expr a) -> Expr a
EWith : FC -> Expr a -> List1 FieldName -> Expr a -> Expr a
EImportAlt : FC -> Expr a -> Expr a -> Expr a
EEmbed : FC -> Import a -> Expr a

Hints:

HasFC (Expr a)
Show (Expr a)