From dc139c90c74c42b7b4cff97bcf431f787dbed62b Mon Sep 17 00:00:00 2001 From: omelkonian Date: Thu, 3 Oct 2024 11:05:18 +0000 Subject: [PATCH] deploy: afb539213772c88f45914b0fbc49df6917ad4701 --- _sources/features.md.txt | 2 +- features.html | 2 +- searchindex.js | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/_sources/features.md.txt b/_sources/features.md.txt index d7675dd3..4b540cc1 100644 --- a/_sources/features.md.txt +++ b/_sources/features.md.txt @@ -299,7 +299,7 @@ five = (id :: Natural -> Natural) 5 (0-Quantity)= ## 0-Quantity Parameters -Parameters can be annotated with a _quantity_ of either `0` or `ω` (the default quantity is `ω` if no quantity is explicitly annotated). Such parameters are irrelevant to evaluation, so they are irrelevant to the compiled Haskell program, and so agda2hs erases them. +Parameters can be annotated with a _quantity_ of either `0` or `ω` (the default quantity is `ω` if no quantity is explicitly annotated). Parameters annotated with `0` are irrelevant to evaluation, so they are irrelevant to the compiled Haskell program, and so agda2hs erases them. Agda: ```agda diff --git a/features.html b/features.html index 3537138c..8e92ffbf 100644 --- a/features.html +++ b/features.html @@ -391,7 +391,7 @@

Explicit type singatures

0-Quantity Parameters

-

Parameters can be annotated with a quantity of either 0 or ω (the default quantity is ω if no quantity is explicitly annotated). Such parameters are irrelevant to evaluation, so they are irrelevant to the compiled Haskell program, and so agda2hs erases them.

+

Parameters can be annotated with a quantity of either 0 or ω (the default quantity is ω if no quantity is explicitly annotated). Parameters annotated with 0 are irrelevant to evaluation, so they are irrelevant to the compiled Haskell program, and so agda2hs erases them.

Agda:

data GhostInt : Set where
     MakeGhostInt : @0 Int → GhostInt
diff --git a/searchindex.js b/searchindex.js
index a1cbd857..c83f173a 100644
--- a/searchindex.js
+++ b/searchindex.js
@@ -1 +1 @@
-Search.setIndex({"docnames": ["features", "index", "introduction", "tutorials"], "filenames": ["features.md", "index.md", "introduction.md", "tutorials.md"], "titles": ["Features", "agda2hs Documentation", "Introduction", "Tutorials"], "terms": {"By": 0, "all": [0, 2, 3], "follow": [0, 1, 3], "agda": [0, 1, 2, 3], "exampl": [0, 1, 3], "ar": [0, 1, 3], "implicitli": [0, 3], "prefix": 0, "necessari": [0, 3], "snippet": 0, "open": [0, 1, 3], "creat": [0, 1, 3], "synonym": [0, 3], "us": [0, 1, 3], "keyword": [0, 3], "requir": [0, 3], "onli": [0, 3], "simpl": 0, "entri": [0, 3], "int": [0, 3], "list": [0, 3], "string": [0, 3], "compil": [0, 1, 2], "agda2h": 0, "standard": [0, 1, 2, 3], "have": [0, 1, 3], "equival": [0, 3], "nat": [0, 3], "set": [0, 1, 3], "where": [0, 1, 3], "zero": 0, "suc": 0, "you": [0, 1, 2, 3], "can": [0, 1, 2, 3], "also": [0, 1, 2, 3], "polymorph": 0, "tree": [0, 1, 3], "leaf": [0, 1, 3], "branch": [0, 3], "unsupport": 0, "term": 0, "index": 0, "definit": [0, 3], "repres": [0, 3], "side": [0, 1, 3], "citat": 0, "id": 0, "author": 0, "titl": 0, "url": 0, "year": 0, "public": 0, "ad": [0, 1, 2, 3], "annot": [0, 1, 3], "pragma": [0, 3], "mkindex": 0, "pair": 0, "b": [0, 3], "mkpair": 0, "show": [0, 1, 3], "eq": [0, 3], "ident": 0, "constructor": 0, "mkident": 0, "runident": 0, "eras": [0, 3], "proof": [0, 1, 3], "equal": [0, 3], "mkequal": 0, "fst": 0, "snd": 0, "unfortun": [0, 3], "doe": [0, 3], "allow": [0, 3], "name": [0, 2, 3], "same": [0, 3], "howev": [0, 3], "i": [0, 1, 2, 3], "possibl": [0, 3], "achiev": [0, 3], "thi": [0, 1, 2, 3], "do": [0, 3], "explicitli": [0, 3], "add": [0, 1, 3], "syntax": [0, 3], "duo": 0, "createduo": 0, "foreign": 0, "lambdacas": 0, "negat": 0, "bool": [0, 3], "true": [0, 1, 3], "fals": [0, 3], "x": [0, 1, 3], "case": [0, 3], "\u03bb": [0, 3], "provid": [0, 1, 3], "nativ": 0, "support": [0, 1, 3], "if_then_else_": 0, "case_of_": 0, "construct": [0, 3], "ifthenels": 0, "n": 0, "10": 0, "big": 0, "els": [0, 3], "small": 0, "mhead": 0, "mayb": [0, 3], "noth": [0, 3], "_": [0, 1, 3], "just": [0, 3], "It": [0, 1, 3], "NOT": 0, "appli": [0, 3], "two": [0, 3], "mean": 0, "must": 0, "write": [0, 1, 2, 3], "2": [0, 2, 3], "3": 0, "instead": [0, 1, 3], "if_then": 0, "copi": 0, "imposs": 0, "second": [0, 3], "while": [0, 3], "thing": [0, 3], "never": 0, "when": [0, 3], "contain": [0, 3], "condit": [0, 3], "which": [0, 1, 2, 3], "split": [0, 3], "e": 0, "know": 0, "The": [0, 1, 3], "signatur": [0, 3], "both": [0, 3], "work": [0, 3], "g": 0, "intrins": 0, "verif": [0, 3], "code": [0, 1, 3], "check": [0, 3], "rang": 0, "mkrang": 0, "low": 0, "high": 0, "h": [0, 2, 3], "createrang": 0, "createrangecas": 0, "simplifi": [0, 3], "": [0, 1, 3], "prim": [0, 3], "five": 0, "5": [0, 2], "natur": [0, 3], "either": 0, "\u03c9": 0, "Such": 0, "irrelev": [0, 3], "evalu": [0, 3], "so": [0, 1, 3], "thei": [0, 3], "program": [0, 1, 2, 3], "them": [0, 3], "ghostint": 0, "makeghostint": 0, "fail": 0, "fromghostint": 0, "pass": 0, "addghostint": 0, "j": 0, "stream": 0, "size": 0, "nil": 0, "con": 0, "thunk": 0, "repeat": 0, "forc": 0, "To": [0, 2, 3], "an": [0, 1, 3], "simpli": [0, 3], "circl": 0, "mkcircl": 0, "radiu": 0, "icircleeq": 0, "r1": 0, "r2": 0, "In": [0, 3], "some": [0, 1, 3], "especi": 0, "might": [0, 3], "properti": [0, 1, 3], "law": [0, 1, 3], "should": [0, 1, 3], "uphold": 0, "islaw": 0, "constructequ": 0, "ieqa": 0, "islawfuleq": 0, "c": [0, 3], "d": 0, "ilawfulcircleeq": 0, "isequ": 0, "ofi": 0, "cong": 0, "ofn": 0, "ceq": 0, "nequal": 0, "constructequalcircl": 0, "class1": 0, "field1": 0, "class2": 0, "field2": 0, "impli": 0, "overlap": 0, "super": 0, "classa": 0, "ord": [0, 1, 3], "ord\u2081": 0, "y": [0, 1, 3], "ord\u2082": 0, "flip": 0, "minim": [0, 3], "full": [0, 1], "gener": [0, 3], "defin": [0, 3], "hasid": 0, "unithasid": 0, "If": [0, 1, 3], "need": [0, 3], "claus": 0, "planet": 0, "mercuri": 0, "venu": 0, "earth": 0, "mar": 0, "jupit": 0, "saturn": 0, "uranu": 0, "neptun": 0, "pluto": 0, "read": [0, 1], "includ": [0, 2, 3], "standalon": 0, "make": [0, 3], "avail": 0, "postul": [0, 3], "iplaneteq": 0, "iplanetord": 0, "more": [0, 3], "complic": [0, 3], "below": 0, "option": [0, 2], "Of": 0, "empti": [0, 3], "ioptionaleq": 0, "Or": 0, "even": [0, 3], "strategi": 0, "specifi": [0, 3], "within": 0, "automat": [0, 3], "flag": [0, 3], "iplanetshow": 0, "stock": 0, "clazz": 0, "foo": 0, "bar": 0, "iplanetclazz": 0, "anyclass": 0, "mkduo": 0, "iduoeq": 0, "standalonederiv": 0, "derivingstrategi": 0, "deriveanyclass": 0, "generalizednewtypederiv": 0, "add1": 0, "1": [0, 3], "odd": 0, "map": [0, 3], "k": [0, 1], "bin": 0, "sz": 0, "kx": 0, "l": [0, 1, 3], "r": [0, 1], "szval": 0, "tip": 0, "implicitfield": 0, "afield": 0, "animplicitfield": 0, "infer": [0, 3], "enabl": [0, 3], "A": [0, 3], "manual": [0, 3], "statement": [0, 3], "anywher": [0, 3], "file": [0, 2, 3], "place": [0, 3], "top": [0, 3], "m1": 0, "mka": 0, "m2": 0, "mkb": 0, "note": [0, 3], "indic": 0, "identifi": 0, "qualifi": 0, "hidden": 0, "although": 0, "one": [0, 3], "still": 0, "mymodul": 0, "m": 0, "test": [0, 2], "other": [0, 1, 3], "insert": 0, "packag": 0, "built": [0, 1], "share": 0, "across": 0, "differ": [0, 3], "modul": [0, 1, 3], "common": [0, 1], "namespac": [0, 1], "pre": 0, "numer": 0, "multipl": 0, "qualif": 0, "absorb": 0, "singl": [0, 3], "specif": [0, 3], "lexicograph": 0, "smallest": 0, "base": [0, 3], "each": [0, 3], "charact": 0, "ascii": 0, "independ": [0, 3], "order": [0, 3], "appear": 0, "sourc": [0, 3], "testc": 0, "testa": 0, "testb": 0, "user": 0, "through": 0, "yaml": 0, "configur": 0, "config": [0, 2], "particularli": 0, "project": [0, 1, 3], "depend": [0, 2], "larg": [0, 1], "librari": [0, 1, 2], "compat": [0, 1], "want": [0, 1, 3], "entir": 0, "mai": 0, "reli": 0, "help": 0, "translat": [0, 1], "ones": 0, "those": [0, 3], "written": [0, 3], "yourself": 0, "latter": [0, 3], "next": [0, 3], "your": [0, 1, 3], "custom": 0, "extent": 0, "compromis": 0, "mathemat": 0, "proven": [0, 3], "correct": [0, 1, 3], "But": [0, 3], "trust": 0, "origin": 0, "problem": 0, "prove": [0, 1], "safe": 0, "For": [0, 1, 3], "let": [0, 1, 2, 3], "suppos": 0, "we": [0, 3], "\u2115": 0, "integ": 0, "\u2124": 0, "ration": 0, "unnormalis": 0, "\u211a": 0, "doubl": [0, 3], "\u211a\u1d58": 0, "p": 0, "denomin": 0, "from": [0, 1, 3], "baseexampl": 0, "twodenom": 0, "output": [0, 3], "would": [0, 1, 3], "po": 0, "here": [0, 3], "doesn": [0, 3], "t": [0, 3], "find": 0, "leav": 0, "run": [0, 3], "again": [0, 3], "builtin": 0, "tointeg": 0, "ratio": 0, "denominatorminus1": 0, "bit": [0, 3], "difficult": 0, "verbos": 0, "level": [0, 3], "26": 0, "log": 0, "part": [0, 3], "begin": [0, 3], "now": [0, 3], "With": [0, 3], "like": [0, 3], "ghci": 0, "accept": 0, "fromintegr": 0, "see": [0, 1, 2, 3], "root": [0, 3], "repositori": [0, 2], "collect": 0, "behaviour": 0, "format": [0, 2], "first": [0, 3], "how": 0, "hide": 0, "seq": 0, "num": 0, "Then": 0, "themselv": 0, "everyth": 0, "get": [0, 3], "except": 0, "caus": [0, 3], "clash": 0, "reus": 0, "henc": 0, "opportun": [0, 3], "revert": 0, "tri": 0, "itself": 0, "choos": 0, "signum": 0, "ghc": [0, 1], "complain": 0, "cannot": [0, 3], "chang": 0, "version": [0, 2, 3], "argument": [0, 3], "modal": 0, "without": [0, 1, 3], "useless": 0, "ha": [0, 3], "its": [0, 3], "remain": [0, 3], "probabl": 0, "becaus": [0, 3], "happen": 0, "after": [0, 3], "sinc": [0, 3], "typecheck": 0, "binari": [0, 1], "readili": 0, "exist": 0, "instal": [0, 3], "path": [0, 2, 3], "call": 0, "setup": 0, "agda2": 0, "variabl": [0, 3], "altern": [0, 3], "hand": [0, 3], "abl": [0, 3], "backend": [0, 1], "insid": [0, 3], "under": [0, 1, 3], "separ": 0, "directori": [0, 2], "yet": [0, 1, 3], "tool": [1, 2], "produc": 1, "verifi": [1, 3], "readabl": 1, "haskel": [1, 2, 3], "extract": [1, 3], "lightli": 1, "encod": 1, "well": 1, "form": 1, "search": 1, "import": [1, 2, 3], "prelud": [1, 2, 3], "data": [1, 3], "bst": 1, "0": [1, 3], "lower": 1, "upper": 1, "pf": 1, "node": 1, "datatyp": [1, 3], "intend": 1, "togeth": 1, "implement": 1, "subset": 1, "reason": [1, 3], "about": [1, 3], "function": 1, "goal": [1, 3], "arbitrari": [1, 3], "rather": 1, "carv": 1, "out": [1, 3], "sublanguag": 1, "between": [1, 3], "straightforward": [1, 3], "fragment": 1, "nice": 1, "look": [1, 3], "colleagu": 1, "shame": 1, "runnabl": 1, "malonzo": 1, "current": [1, 3], "progress": 1, "been": 1, "contribut": 1, "wai": [1, 3], "veri": 1, "welcom": 1, "wa": [1, 3], "introduc": 1, "symposium": 1, "22": 1, "paper": 1, "activ": 1, "develop": 1, "pleas": 1, "take": [1, 3], "issu": [1, 3], "tracker": 1, "suggest": 1, "new": [1, 3], "featur": [1, 3], "pr": 1, "request": 1, "abov": 1, "advis": 1, "introduct": 1, "rewrit": 1, "rule": [1, 3], "emac": 1, "mode": [1, 3], "tutori": 1, "languag": 2, "6": 2, "4": 2, "lib": [2, 3], "navig": 2, "html": 2, "along": 2, "comprehens": 2, "suit": 2, "releas": 2, "hackag": 2, "onc": [2, 3], "bundl": 2, "regist": 2, "locat": 2, "command": 2, "libari": 2, "default": 2, "global": 2, "echo": 2, "dir": 2, "shell": 2, "clone": 2, "local": 2, "git": 2, "github": [2, 3], "com": 2, "build": 2, "cd": 2, "pwd": 2, "o": [2, 3], "outputdir": 2, "modulepath": 2, "todo": 2, "integr": 2, "preprocessor": 2, "relev": 3, "found": 3, "time": 3, "folder": 3, "basic": 3, "describ": 3, "document": 3, "minimum": 3, "least": 3, "helloworld": 3, "detail": 3, "our": 3, "erasur": 3, "label": 3, "toi": 3, "perfectli": 3, "handi": 3, "src": 3, "far": 3, "live": 3, "final": 3, "type": 3, "line": 3, "strictli": 3, "miss": 3, "confin": 3, "result": 3, "incorrect": 3, "encapsul": 3, "properli": 3, "good": 3, "practic": 3, "access": 3, "come": 3, "meaningless": 3, "everi": 3, "skip": 3, "dure": 3, "misspel": 3, "warn": 3, "continu": 3, "proceed": 3, "load": 3, "expect": 3, "ideal": 3, "than": 3, "intuit": 3, "codebas": 3, "resid": 3, "reflect": 3, "declar": 3, "countdown": 3, "usag": 3, "usual": 3, "give": 3, "interact": 3, "ani": 3, "likewis": 3, "target": 3, "principl": 3, "invok": 3, "basi": 3, "whole": 3, "addit": 3, "script": 3, "former": 3, "thu": 3, "execut": 3, "sh": 3, "aim": 3, "explain": 3, "formal": 3, "techniqu": 3, "compliant": 3, "section": 3, "triangl": 3, "sai": 3, "attempt": 3, "somewhat": 3, "mktriangl": 3, "alpha": 3, "beta": 3, "gamma": 3, "three": 3, "angl": 3, "thats": 3, "interest": 3, "valu": 3, "neg": 3, "easier": 3, "number": 3, "enough": 3, "constitut": 3, "sum": 3, "up": 3, "180": 3, "degre": 3, "most": 3, "right": 3, "obtus": 3, "model": 3, "countbiggerthan": 3, "length": 3, "filter": 3, "h\u2081": 3, "90": 3, "hypothes": 3, "trick": 3, "notic": 3, "bracket": 3, "signifi": 3, "instanc": 3, "present": 3, "context": 3, "These": 3, "therefor": 3, "done": 3, "quantiti": 3, "paramet": 3, "correctli": 3, "hypothesi": 3, "helper": 3, "could": 3, "oper": 3, "sole": 3, "anoth": 3, "typeclass": 3, "ask": 3, "point": 3, "anywai": 3, "remaind": 3, "inde": 3, "createtriangl": 3, "exactli": 3, "shape": 3, "perceiv": 3, "redund": 3, "chain": 3, "AND": 3, "refer": 3, "seen": 3, "createtriangle\u2081": 3, "righttru": 3, "lefttru": 3, "offer": 3, "much": 3, "cleaner": 3, "nest": 3, "messier": 3, "worth": 3, "assert": 3, "rewritten": 3, "anonym": 3, "secondli": 3, "curli": 3, "lastli": 3, "compound": 3, "were": 3, "mani": 3, "theorem": 3, "design": 3, "own": 3, "expand": 3, "ascend": 3, "try": 3, "u": 3, "later": 3, "judgment": 3, "isascend": 3, "iorda": 3, "input": 3, "further": 3, "better": 3, "isascending\u2082": 3, "oneelem": 3, "manyelem": 3, "istru": 3, "match": 3, "amount": 3, "per": 3, "occur": 3, "materi": 3, "relat": 3, "return": 3, "hold": 3, "vice": 3, "versa": 3, "direct": 3, "proof\u2081": 3, "assist": 3, "question": 3, "mark": 3, "seamlessli": 3, "preview": 3, "guid": 3, "trivial": 3, "itstru": 3, "x\u2081": 3, "h\u2082": 3, "third": 3, "insight": 3, "implicit": 3, "state": 3, "easili": 3, "transform": 3, "equat": 3, "step": 3, "until": 3, "obtain": 3, "given": 3, "useeq": 3, "reverseeq": 3, "refl": 3, "sym": 3, "iftrueeqthen": 3, "had": 3, "though": 3, "proper": 3, "inspect": 3, "revers": 3, "iff": 3, "substanti": 3, "discuss": 3, "reductio": 3, "absurdum": 3, "absurd\u2081": 3, "tactic": 3, "deal": 3, "self": 3, "contradictori": 3, "contradict": 3, "discard": 3, "absurd": 3, "aris": 3, "combin": 3, "method": 3, "induct": 3, "helper\u2081": 3, "magic": 3, "pattern": 3, "narrow": 3, "down": 3, "save": 3, "resolv": 3, "intern": 3, "theorem\u2082": 3, "h\u2083": 3, "theorem\u2082help": 3, "recurs": 3, "postulate3": 3, "actual": 3, "attach": 3, "bad": 3, "termin": 3, "did": 3, "recogn": 3, "being": 3, "invalid": 3, "turn": 3, "known": 3, "abstract": 3, "rid": 3, "helper\u2082": 3, "theorem\u2083": 3, "tail": 3, "thank": 3, "approach": 3, "remov": 3, "On": 3, "break": 3, "wouldn": 3, "last": 3, "style": 3, "clear": 3, "demonstr": 3, "class": 3, "concept": 3, "shouldn": 3}, "objects": {}, "objtypes": {}, "objnames": {}, "titleterms": {"featur": 0, "data": 0, "type": 0, "declar": 0, "datatyp": 0, "record": 0, "newtyp": 0, "pattern": 0, "match": 0, "valu": 0, "flow": 0, "control": 0, "wit": 0, "explicit": 0, "singatur": 0, "0": 0, "quantiti": 0, "paramet": 0, "coinduct": 0, "class": 0, "constrain": 0, "typeclass": 0, "instanc": 0, "default": 0, "field": 0, "implement": 0, "copattern": 0, "deriv": 0, "partial": 0, "applic": 0, "mutual": 0, "recurs": 0, "function": [0, 3], "implicit": 0, "haskel": 0, "languag": 0, "extens": 0, "import": 0, "rewrit": 0, "rule": 0, "prelud": 0, "handl": 0, "known": 0, "issu": 0, "emac": 0, "mode": 0, "agda2h": [1, 2, 3], "document": 1, "object": 1, "futur": 1, "work": 1, "content": 1, "introduct": 2, "get": 2, "start": 2, "requir": 2, "instal": 2, "cabal": 2, "manual": 2, "run": 2, "us": 2, "stack": 2, "tutori": 3, "how": 3, "build": 3, "small": 3, "librari": 3, "compil": 3, "manag": 3, "structur": 3, "depend": 3, "bigger": 3, "repositori": 3, "what": 3, "prove": 3, "constructor": 3, "constraint": 3, "predic": 3}, "envversion": {"sphinx.domains.c": 2, "sphinx.domains.changeset": 1, "sphinx.domains.citation": 1, "sphinx.domains.cpp": 8, "sphinx.domains.index": 1, "sphinx.domains.javascript": 2, "sphinx.domains.math": 2, "sphinx.domains.python": 3, "sphinx.domains.rst": 2, "sphinx.domains.std": 2, "sphinx": 57}, "alltitles": {"Features": [[0, "features"]], "Data & Type Declarations": [[0, "data-type-declarations"]], "Types": [[0, "types"]], "Datatypes": [[0, "datatypes"]], "Records": [[0, "records"]], "Newtypes": [[0, "newtypes"]], "Pattern Matching on Datatype Values": [[0, "pattern-matching-on-datatype-values"]], "Flow Control": [[0, "flow-control"]], "Flow Witnesses": [[0, "flow-witnesses"]], "Explicit type singatures": [[0, "explicit-type-singatures"]], "0-Quantity Parameters": [[0, "quantity-parameters"]], "Coinduction": [[0, "coinduction"]], "Type Classes": [[0, "type-classes"]], "Constrained Typeclass Instance": [[0, "constrained-typeclass-instance"]], "Constrained Typeclass": [[0, "constrained-typeclass"]], "Default Typeclass Field Implementations": [[0, "default-typeclass-field-implementations"]], "Copatterns in Type Class Instances": [[0, "copatterns-in-type-class-instances"]], "Deriving Type Class Instances": [[0, "deriving-type-class-instances"]], "Partial Application": [[0, "partial-application"]], "Mutual Recursion": [[0, "mutual-recursion"]], "Mutually Recursive Functions": [[0, "mutually-recursive-functions"]], "Mutually Recursive Datatype and Function": [[0, "mutually-recursive-datatype-and-function"]], "Implicit Record Field": [[0, "implicit-record-field"]], "Haskell Language Extensions": [[0, "haskell-language-extensions"]], "Imports": [[0, "imports"]], "Rewrite rules and Prelude imports": [[0, "rewrite-rules-and-prelude-imports"]], "Rewrite rules": [[0, "rewrite-rules"]], "Handling of Prelude": [[0, "handling-of-prelude"]], "Known issues": [[0, "known-issues"], [0, "id1"]], "Emacs mode": [[0, "emacs-mode"]], "agda2hs Documentation": [[1, "agda2hs-documentation"]], "Objective": [[1, "objective"]], "Documentation": [[1, "documentation"]], "Future work": [[1, "future-work"]], "Contents": [[1, null]], "Introduction": [[2, "introduction"]], "Getting Started": [[2, "getting-started"]], "Requirements": [[2, "requirements"]], "Installation with Cabal": [[2, "installation-with-cabal"]], "Manual installation": [[2, "manual-installation"]], "Running agda2hs": [[2, "running-agda2hs"]], "Using agda2hs with Stack": [[2, "using-agda2hs-with-stack"]], "Tutorials": [[3, "tutorials"]], "How to build a small library in agda2hs": [[3, "how-to-build-a-small-library-in-agda2hs"]], "Compilation": [[3, "compilation"], [3, "id1"]], "How to manage structure and dependencies of a bigger repository?": [[3, "how-to-manage-structure-and-dependencies-of-a-bigger-repository"]], "How (and what) to prove?": [[3, "how-and-what-to-prove"]], "Constructor constraints": [[3, "constructor-constraints"]], "Function or Predicate?": [[3, "function-or-predicate"]]}, "indexentries": {}})
\ No newline at end of file
+Search.setIndex({"docnames": ["features", "index", "introduction", "tutorials"], "filenames": ["features.md", "index.md", "introduction.md", "tutorials.md"], "titles": ["Features", "agda2hs Documentation", "Introduction", "Tutorials"], "terms": {"By": 0, "all": [0, 2, 3], "follow": [0, 1, 3], "agda": [0, 1, 2, 3], "exampl": [0, 1, 3], "ar": [0, 1, 3], "implicitli": [0, 3], "prefix": 0, "necessari": [0, 3], "snippet": 0, "open": [0, 1, 3], "creat": [0, 1, 3], "synonym": [0, 3], "us": [0, 1, 3], "keyword": [0, 3], "requir": [0, 3], "onli": [0, 3], "simpl": 0, "entri": [0, 3], "int": [0, 3], "list": [0, 3], "string": [0, 3], "compil": [0, 1, 2], "agda2h": 0, "standard": [0, 1, 2, 3], "have": [0, 1, 3], "equival": [0, 3], "nat": [0, 3], "set": [0, 1, 3], "where": [0, 1, 3], "zero": 0, "suc": 0, "you": [0, 1, 2, 3], "can": [0, 1, 2, 3], "also": [0, 1, 2, 3], "polymorph": 0, "tree": [0, 1, 3], "leaf": [0, 1, 3], "branch": [0, 3], "unsupport": 0, "term": 0, "index": 0, "definit": [0, 3], "repres": [0, 3], "side": [0, 1, 3], "citat": 0, "id": 0, "author": 0, "titl": 0, "url": 0, "year": 0, "public": 0, "ad": [0, 1, 2, 3], "annot": [0, 1, 3], "pragma": [0, 3], "mkindex": 0, "pair": 0, "b": [0, 3], "mkpair": 0, "show": [0, 1, 3], "eq": [0, 3], "ident": 0, "constructor": 0, "mkident": 0, "runident": 0, "eras": [0, 3], "proof": [0, 1, 3], "equal": [0, 3], "mkequal": 0, "fst": 0, "snd": 0, "unfortun": [0, 3], "doe": [0, 3], "allow": [0, 3], "name": [0, 2, 3], "same": [0, 3], "howev": [0, 3], "i": [0, 1, 2, 3], "possibl": [0, 3], "achiev": [0, 3], "thi": [0, 1, 2, 3], "do": [0, 3], "explicitli": [0, 3], "add": [0, 1, 3], "syntax": [0, 3], "duo": 0, "createduo": 0, "foreign": 0, "lambdacas": 0, "negat": 0, "bool": [0, 3], "true": [0, 1, 3], "fals": [0, 3], "x": [0, 1, 3], "case": [0, 3], "\u03bb": [0, 3], "provid": [0, 1, 3], "nativ": 0, "support": [0, 1, 3], "if_then_else_": 0, "case_of_": 0, "construct": [0, 3], "ifthenels": 0, "n": 0, "10": 0, "big": 0, "els": [0, 3], "small": 0, "mhead": 0, "mayb": [0, 3], "noth": [0, 3], "_": [0, 1, 3], "just": [0, 3], "It": [0, 1, 3], "NOT": 0, "appli": [0, 3], "two": [0, 3], "mean": 0, "must": 0, "write": [0, 1, 2, 3], "2": [0, 2, 3], "3": 0, "instead": [0, 1, 3], "if_then": 0, "copi": 0, "imposs": 0, "second": [0, 3], "while": [0, 3], "thing": [0, 3], "never": 0, "when": [0, 3], "contain": [0, 3], "condit": [0, 3], "which": [0, 1, 2, 3], "split": [0, 3], "e": 0, "know": 0, "The": [0, 1, 3], "signatur": [0, 3], "both": [0, 3], "work": [0, 3], "g": 0, "intrins": 0, "verif": [0, 3], "code": [0, 1, 3], "check": [0, 3], "rang": 0, "mkrang": 0, "low": 0, "high": 0, "h": [0, 2, 3], "createrang": 0, "createrangecas": 0, "simplifi": [0, 3], "": [0, 1, 3], "prim": [0, 3], "five": 0, "5": [0, 2], "natur": [0, 3], "either": 0, "\u03c9": 0, "irrelev": [0, 3], "evalu": [0, 3], "so": [0, 1, 3], "thei": [0, 3], "program": [0, 1, 2, 3], "them": [0, 3], "ghostint": 0, "makeghostint": 0, "fail": 0, "fromghostint": 0, "pass": 0, "addghostint": 0, "j": 0, "stream": 0, "size": 0, "nil": 0, "con": 0, "thunk": 0, "repeat": 0, "forc": 0, "To": [0, 2, 3], "an": [0, 1, 3], "simpli": [0, 3], "circl": 0, "mkcircl": 0, "radiu": 0, "icircleeq": 0, "r1": 0, "r2": 0, "In": [0, 3], "some": [0, 1, 3], "especi": 0, "might": [0, 3], "properti": [0, 1, 3], "law": [0, 1, 3], "should": [0, 1, 3], "uphold": 0, "islaw": 0, "constructequ": 0, "ieqa": 0, "islawfuleq": 0, "c": [0, 3], "d": 0, "ilawfulcircleeq": 0, "isequ": 0, "ofi": 0, "cong": 0, "ofn": 0, "ceq": 0, "nequal": 0, "constructequalcircl": 0, "class1": 0, "field1": 0, "class2": 0, "field2": 0, "impli": 0, "overlap": 0, "super": 0, "classa": 0, "ord": [0, 1, 3], "ord\u2081": 0, "y": [0, 1, 3], "ord\u2082": 0, "flip": 0, "minim": [0, 3], "full": [0, 1], "gener": [0, 3], "defin": [0, 3], "hasid": 0, "unithasid": 0, "If": [0, 1, 3], "need": [0, 3], "claus": 0, "planet": 0, "mercuri": 0, "venu": 0, "earth": 0, "mar": 0, "jupit": 0, "saturn": 0, "uranu": 0, "neptun": 0, "pluto": 0, "read": [0, 1], "includ": [0, 2, 3], "standalon": 0, "make": [0, 3], "avail": 0, "postul": [0, 3], "iplaneteq": 0, "iplanetord": 0, "more": [0, 3], "complic": [0, 3], "below": 0, "option": [0, 2], "Of": 0, "empti": [0, 3], "ioptionaleq": 0, "Or": 0, "even": [0, 3], "strategi": 0, "specifi": [0, 3], "within": 0, "automat": [0, 3], "flag": [0, 3], "iplanetshow": 0, "stock": 0, "clazz": 0, "foo": 0, "bar": 0, "iplanetclazz": 0, "anyclass": 0, "mkduo": 0, "iduoeq": 0, "standalonederiv": 0, "derivingstrategi": 0, "deriveanyclass": 0, "generalizednewtypederiv": 0, "add1": 0, "1": [0, 3], "odd": 0, "map": [0, 3], "k": [0, 1], "bin": 0, "sz": 0, "kx": 0, "l": [0, 1, 3], "r": [0, 1], "szval": 0, "tip": 0, "implicitfield": 0, "afield": 0, "animplicitfield": 0, "infer": [0, 3], "enabl": [0, 3], "A": [0, 3], "manual": [0, 3], "statement": [0, 3], "anywher": [0, 3], "file": [0, 2, 3], "place": [0, 3], "top": [0, 3], "m1": 0, "mka": 0, "m2": 0, "mkb": 0, "note": [0, 3], "indic": 0, "identifi": 0, "qualifi": 0, "hidden": 0, "although": 0, "one": [0, 3], "still": 0, "mymodul": 0, "m": 0, "test": [0, 2], "other": [0, 1, 3], "insert": 0, "packag": 0, "built": [0, 1], "share": 0, "across": 0, "differ": [0, 3], "modul": [0, 1, 3], "common": [0, 1], "namespac": [0, 1], "pre": 0, "numer": 0, "multipl": 0, "qualif": 0, "absorb": 0, "singl": [0, 3], "specif": [0, 3], "lexicograph": 0, "smallest": 0, "base": [0, 3], "each": [0, 3], "charact": 0, "ascii": 0, "independ": [0, 3], "order": [0, 3], "appear": 0, "sourc": [0, 3], "testc": 0, "testa": 0, "testb": 0, "user": 0, "through": 0, "yaml": 0, "configur": 0, "config": [0, 2], "particularli": 0, "project": [0, 1, 3], "depend": [0, 2], "larg": [0, 1], "librari": [0, 1, 2], "compat": [0, 1], "want": [0, 1, 3], "entir": 0, "mai": 0, "reli": 0, "help": 0, "translat": [0, 1], "ones": 0, "those": [0, 3], "written": [0, 3], "yourself": 0, "latter": [0, 3], "next": [0, 3], "your": [0, 1, 3], "custom": 0, "extent": 0, "compromis": 0, "mathemat": 0, "proven": [0, 3], "correct": [0, 1, 3], "But": [0, 3], "trust": 0, "origin": 0, "problem": 0, "prove": [0, 1], "safe": 0, "For": [0, 1, 3], "let": [0, 1, 2, 3], "suppos": 0, "we": [0, 3], "\u2115": 0, "integ": 0, "\u2124": 0, "ration": 0, "unnormalis": 0, "\u211a": 0, "doubl": [0, 3], "\u211a\u1d58": 0, "p": 0, "denomin": 0, "from": [0, 1, 3], "baseexampl": 0, "twodenom": 0, "output": [0, 3], "would": [0, 1, 3], "po": 0, "here": [0, 3], "doesn": [0, 3], "t": [0, 3], "find": 0, "leav": 0, "run": [0, 3], "again": [0, 3], "builtin": 0, "tointeg": 0, "ratio": 0, "denominatorminus1": 0, "bit": [0, 3], "difficult": 0, "verbos": 0, "level": [0, 3], "26": 0, "log": 0, "part": [0, 3], "begin": [0, 3], "now": [0, 3], "With": [0, 3], "like": [0, 3], "ghci": 0, "accept": 0, "fromintegr": 0, "see": [0, 1, 2, 3], "root": [0, 3], "repositori": [0, 2], "collect": 0, "behaviour": 0, "format": [0, 2], "first": [0, 3], "how": 0, "hide": 0, "seq": 0, "num": 0, "Then": 0, "themselv": 0, "everyth": 0, "get": [0, 3], "except": 0, "caus": [0, 3], "clash": 0, "reus": 0, "henc": 0, "opportun": [0, 3], "revert": 0, "tri": 0, "itself": 0, "choos": 0, "signum": 0, "ghc": [0, 1], "complain": 0, "cannot": [0, 3], "chang": 0, "version": [0, 2, 3], "argument": [0, 3], "modal": 0, "without": [0, 1, 3], "useless": 0, "ha": [0, 3], "its": [0, 3], "remain": [0, 3], "probabl": 0, "becaus": [0, 3], "happen": 0, "after": [0, 3], "sinc": [0, 3], "typecheck": 0, "binari": [0, 1], "readili": 0, "exist": 0, "instal": [0, 3], "path": [0, 2, 3], "call": 0, "setup": 0, "agda2": 0, "variabl": [0, 3], "altern": [0, 3], "hand": [0, 3], "abl": [0, 3], "backend": [0, 1], "insid": [0, 3], "under": [0, 1, 3], "separ": 0, "directori": [0, 2], "yet": [0, 1, 3], "tool": [1, 2], "produc": 1, "verifi": [1, 3], "readabl": 1, "haskel": [1, 2, 3], "extract": [1, 3], "lightli": 1, "encod": 1, "well": 1, "form": 1, "search": 1, "import": [1, 2, 3], "prelud": [1, 2, 3], "data": [1, 3], "bst": 1, "0": [1, 3], "lower": 1, "upper": 1, "pf": 1, "node": 1, "datatyp": [1, 3], "intend": 1, "togeth": 1, "implement": 1, "subset": 1, "reason": [1, 3], "about": [1, 3], "function": 1, "goal": [1, 3], "arbitrari": [1, 3], "rather": 1, "carv": 1, "out": [1, 3], "sublanguag": 1, "between": [1, 3], "straightforward": [1, 3], "fragment": 1, "nice": 1, "look": [1, 3], "colleagu": 1, "shame": 1, "runnabl": 1, "malonzo": 1, "current": [1, 3], "progress": 1, "been": 1, "contribut": 1, "wai": [1, 3], "veri": 1, "welcom": 1, "wa": [1, 3], "introduc": 1, "symposium": 1, "22": 1, "paper": 1, "activ": 1, "develop": 1, "pleas": 1, "take": [1, 3], "issu": [1, 3], "tracker": 1, "suggest": 1, "new": [1, 3], "featur": [1, 3], "pr": 1, "request": 1, "abov": 1, "advis": 1, "introduct": 1, "rewrit": 1, "rule": [1, 3], "emac": 1, "mode": [1, 3], "tutori": 1, "languag": 2, "6": 2, "4": 2, "lib": [2, 3], "navig": 2, "html": 2, "along": 2, "comprehens": 2, "suit": 2, "releas": 2, "hackag": 2, "onc": [2, 3], "bundl": 2, "regist": 2, "locat": 2, "command": 2, "libari": 2, "default": 2, "global": 2, "echo": 2, "dir": 2, "shell": 2, "clone": 2, "local": 2, "git": 2, "github": [2, 3], "com": 2, "build": 2, "cd": 2, "pwd": 2, "o": [2, 3], "outputdir": 2, "modulepath": 2, "todo": 2, "integr": 2, "preprocessor": 2, "relev": 3, "found": 3, "time": 3, "folder": 3, "basic": 3, "describ": 3, "document": 3, "minimum": 3, "least": 3, "helloworld": 3, "detail": 3, "our": 3, "erasur": 3, "label": 3, "toi": 3, "perfectli": 3, "handi": 3, "src": 3, "far": 3, "live": 3, "final": 3, "type": 3, "line": 3, "strictli": 3, "miss": 3, "confin": 3, "result": 3, "incorrect": 3, "encapsul": 3, "properli": 3, "good": 3, "practic": 3, "access": 3, "come": 3, "meaningless": 3, "everi": 3, "skip": 3, "dure": 3, "misspel": 3, "warn": 3, "continu": 3, "proceed": 3, "load": 3, "expect": 3, "ideal": 3, "than": 3, "intuit": 3, "codebas": 3, "resid": 3, "reflect": 3, "declar": 3, "countdown": 3, "usag": 3, "usual": 3, "give": 3, "interact": 3, "ani": 3, "likewis": 3, "target": 3, "principl": 3, "invok": 3, "basi": 3, "whole": 3, "addit": 3, "script": 3, "former": 3, "thu": 3, "execut": 3, "sh": 3, "aim": 3, "explain": 3, "formal": 3, "techniqu": 3, "compliant": 3, "section": 3, "triangl": 3, "sai": 3, "attempt": 3, "somewhat": 3, "mktriangl": 3, "alpha": 3, "beta": 3, "gamma": 3, "three": 3, "angl": 3, "thats": 3, "interest": 3, "valu": 3, "neg": 3, "easier": 3, "number": 3, "enough": 3, "constitut": 3, "sum": 3, "up": 3, "180": 3, "degre": 3, "most": 3, "right": 3, "obtus": 3, "model": 3, "countbiggerthan": 3, "length": 3, "filter": 3, "h\u2081": 3, "90": 3, "hypothes": 3, "trick": 3, "notic": 3, "bracket": 3, "signifi": 3, "instanc": 3, "present": 3, "context": 3, "These": 3, "therefor": 3, "done": 3, "quantiti": 3, "paramet": 3, "correctli": 3, "hypothesi": 3, "helper": 3, "could": 3, "oper": 3, "sole": 3, "anoth": 3, "typeclass": 3, "ask": 3, "point": 3, "anywai": 3, "remaind": 3, "inde": 3, "createtriangl": 3, "exactli": 3, "shape": 3, "perceiv": 3, "redund": 3, "chain": 3, "AND": 3, "refer": 3, "seen": 3, "createtriangle\u2081": 3, "righttru": 3, "lefttru": 3, "offer": 3, "much": 3, "cleaner": 3, "nest": 3, "messier": 3, "worth": 3, "assert": 3, "rewritten": 3, "anonym": 3, "secondli": 3, "curli": 3, "lastli": 3, "compound": 3, "were": 3, "mani": 3, "theorem": 3, "design": 3, "own": 3, "expand": 3, "ascend": 3, "try": 3, "u": 3, "later": 3, "judgment": 3, "isascend": 3, "iorda": 3, "input": 3, "further": 3, "better": 3, "isascending\u2082": 3, "oneelem": 3, "manyelem": 3, "istru": 3, "match": 3, "amount": 3, "per": 3, "occur": 3, "materi": 3, "relat": 3, "return": 3, "hold": 3, "vice": 3, "versa": 3, "direct": 3, "proof\u2081": 3, "assist": 3, "question": 3, "mark": 3, "seamlessli": 3, "preview": 3, "guid": 3, "trivial": 3, "itstru": 3, "x\u2081": 3, "h\u2082": 3, "third": 3, "insight": 3, "implicit": 3, "state": 3, "easili": 3, "transform": 3, "equat": 3, "step": 3, "until": 3, "obtain": 3, "given": 3, "useeq": 3, "reverseeq": 3, "refl": 3, "sym": 3, "iftrueeqthen": 3, "had": 3, "though": 3, "proper": 3, "inspect": 3, "revers": 3, "iff": 3, "substanti": 3, "discuss": 3, "reductio": 3, "absurdum": 3, "absurd\u2081": 3, "tactic": 3, "deal": 3, "self": 3, "contradictori": 3, "contradict": 3, "discard": 3, "absurd": 3, "aris": 3, "combin": 3, "method": 3, "induct": 3, "helper\u2081": 3, "magic": 3, "pattern": 3, "narrow": 3, "down": 3, "save": 3, "resolv": 3, "intern": 3, "theorem\u2082": 3, "h\u2083": 3, "theorem\u2082help": 3, "recurs": 3, "postulate3": 3, "actual": 3, "attach": 3, "bad": 3, "termin": 3, "did": 3, "recogn": 3, "being": 3, "invalid": 3, "turn": 3, "known": 3, "abstract": 3, "rid": 3, "helper\u2082": 3, "theorem\u2083": 3, "tail": 3, "thank": 3, "approach": 3, "remov": 3, "On": 3, "break": 3, "wouldn": 3, "last": 3, "style": 3, "clear": 3, "demonstr": 3, "class": 3, "concept": 3, "shouldn": 3}, "objects": {}, "objtypes": {}, "objnames": {}, "titleterms": {"featur": 0, "data": 0, "type": 0, "declar": 0, "datatyp": 0, "record": 0, "newtyp": 0, "pattern": 0, "match": 0, "valu": 0, "flow": 0, "control": 0, "wit": 0, "explicit": 0, "singatur": 0, "0": 0, "quantiti": 0, "paramet": 0, "coinduct": 0, "class": 0, "constrain": 0, "typeclass": 0, "instanc": 0, "default": 0, "field": 0, "implement": 0, "copattern": 0, "deriv": 0, "partial": 0, "applic": 0, "mutual": 0, "recurs": 0, "function": [0, 3], "implicit": 0, "haskel": 0, "languag": 0, "extens": 0, "import": 0, "rewrit": 0, "rule": 0, "prelud": 0, "handl": 0, "known": 0, "issu": 0, "emac": 0, "mode": 0, "agda2h": [1, 2, 3], "document": 1, "object": 1, "futur": 1, "work": 1, "content": 1, "introduct": 2, "get": 2, "start": 2, "requir": 2, "instal": 2, "cabal": 2, "manual": 2, "run": 2, "us": 2, "stack": 2, "tutori": 3, "how": 3, "build": 3, "small": 3, "librari": 3, "compil": 3, "manag": 3, "structur": 3, "depend": 3, "bigger": 3, "repositori": 3, "what": 3, "prove": 3, "constructor": 3, "constraint": 3, "predic": 3}, "envversion": {"sphinx.domains.c": 2, "sphinx.domains.changeset": 1, "sphinx.domains.citation": 1, "sphinx.domains.cpp": 8, "sphinx.domains.index": 1, "sphinx.domains.javascript": 2, "sphinx.domains.math": 2, "sphinx.domains.python": 3, "sphinx.domains.rst": 2, "sphinx.domains.std": 2, "sphinx": 57}, "alltitles": {"Features": [[0, "features"]], "Data & Type Declarations": [[0, "data-type-declarations"]], "Types": [[0, "types"]], "Datatypes": [[0, "datatypes"]], "Records": [[0, "records"]], "Newtypes": [[0, "newtypes"]], "Pattern Matching on Datatype Values": [[0, "pattern-matching-on-datatype-values"]], "Flow Control": [[0, "flow-control"]], "Flow Witnesses": [[0, "flow-witnesses"]], "Explicit type singatures": [[0, "explicit-type-singatures"]], "0-Quantity Parameters": [[0, "quantity-parameters"]], "Coinduction": [[0, "coinduction"]], "Type Classes": [[0, "type-classes"]], "Constrained Typeclass Instance": [[0, "constrained-typeclass-instance"]], "Constrained Typeclass": [[0, "constrained-typeclass"]], "Default Typeclass Field Implementations": [[0, "default-typeclass-field-implementations"]], "Copatterns in Type Class Instances": [[0, "copatterns-in-type-class-instances"]], "Deriving Type Class Instances": [[0, "deriving-type-class-instances"]], "Partial Application": [[0, "partial-application"]], "Mutual Recursion": [[0, "mutual-recursion"]], "Mutually Recursive Functions": [[0, "mutually-recursive-functions"]], "Mutually Recursive Datatype and Function": [[0, "mutually-recursive-datatype-and-function"]], "Implicit Record Field": [[0, "implicit-record-field"]], "Haskell Language Extensions": [[0, "haskell-language-extensions"]], "Imports": [[0, "imports"]], "Rewrite rules and Prelude imports": [[0, "rewrite-rules-and-prelude-imports"]], "Rewrite rules": [[0, "rewrite-rules"]], "Handling of Prelude": [[0, "handling-of-prelude"]], "Known issues": [[0, "known-issues"], [0, "id1"]], "Emacs mode": [[0, "emacs-mode"]], "agda2hs Documentation": [[1, "agda2hs-documentation"]], "Objective": [[1, "objective"]], "Documentation": [[1, "documentation"]], "Future work": [[1, "future-work"]], "Contents": [[1, null]], "Introduction": [[2, "introduction"]], "Getting Started": [[2, "getting-started"]], "Requirements": [[2, "requirements"]], "Installation with Cabal": [[2, "installation-with-cabal"]], "Manual installation": [[2, "manual-installation"]], "Running agda2hs": [[2, "running-agda2hs"]], "Using agda2hs with Stack": [[2, "using-agda2hs-with-stack"]], "Tutorials": [[3, "tutorials"]], "How to build a small library in agda2hs": [[3, "how-to-build-a-small-library-in-agda2hs"]], "Compilation": [[3, "compilation"], [3, "id1"]], "How to manage structure and dependencies of a bigger repository?": [[3, "how-to-manage-structure-and-dependencies-of-a-bigger-repository"]], "How (and what) to prove?": [[3, "how-and-what-to-prove"]], "Constructor constraints": [[3, "constructor-constraints"]], "Function or Predicate?": [[3, "function-or-predicate"]]}, "indexentries": {}})
\ No newline at end of file